Własności

start


definition                   definition
  let x1 be Θ1;                 let x1 be Θ1;
  ......                         .........
  let x1 be Θ1;                 let x1 be Θ1;
  <definicja-właściwa>          redefine <redefinicja>. 
  <warunki-poprawn○ości>        <warunki-poprawności>
  własność                        własność
  proof                          proof
     thus φ;                         thus ψ;
  end;                           end;
end;                          end;

gdzie własność to słowo z kolumny własność, φ to formuła z kolumny znaczenie, a ψ to formuła z kolumny redefinicja.

własność znaczenie redefinicja przukłady dotyczy
sethood; ex X st for x being Θ st Φ(x) holds x in X ex X st for y being Θ' holds y in X mmlqury mode, rejestracja dla klastra przymiotników
associativity; nie zaimplementowane mmlqury binary functor
asymmetry; for a,b being Θ st Φ(a,b) holds not Φ(b,a) for a,b being Θ st a ≈ b holds not b ≈ a mmlqury binary predicate
commutativity; for a,b,c being Θ st Φ(a,b,c) holds Φ(b,a.c) for a,b being Θ holds a ⊕ b = b ⊕ a mmlqury binary functor
connectedness; for a,b being Θ holds Φ(a,b) or Φ(b,a) for a,b being Θ holds a ≈ b or b ≈ a mmlqury binary predicate
idempotence; for a being Θ holds Φ(a,a,a) for a being Θ holds a ⊕ a = a mmlqury binary functor
involutiveness; for a,b being Θ st Φ(a,b) holds Φ(b,a) for a being Θ holds ⊕⊕a = a mmlqury unary functor
irreflexivity; for a being Θ holds not Φ(a,a) for a being Θ holds not a ≈ a mmlqury binary predicate
projectivity; for a,b being Θ st Φ(a,b) holds Φ(b,b) for a being Θ holds ⊕⊕a = ⊕a mmlqury unary functor
reflexivity; for a being Θ holds Φ(a,a) for a being Θ holds a ≈ a mmlqury binary predicate
symmetry; for a,b being Θ st Φ(a,b) holds Φ(b,a) for a,b being Θ st a ≈ b holds b ≈ a mmlqury binary predicate
transitivity; nie zaimplementowane -- mmlqury  
WebForm
TopicClassification Select one...
ProjectGroup?

ImplementationDate? N/A
Topic revision: r6 - 2012-01-29 - 17:56:46 - GrzegorzBancerek
Mizar.ManualPlProperty moved from Mizar.ManualPlProperties on 2012-01-22 - 19:04 by GrzegorzBancerek - put it back
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback