Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Galois Connections

**by****Czeslaw Bylinski**- Received September 25, 1996
- MML identifier: WAYBEL_1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, PRE_TOPC, ORDERS_1, SEQM_3, RELAT_2, LATTICE3, LATTICES, WAYBEL_0, YELLOW_1, BOOLE, YELLOW_0, CAT_1, WELLORD1, ORDINAL2, BHSP_3, FILTER_0, FILTER_2, BINOP_1, SGRAPH1, GROUP_6, QUANTAL1, YELLOW_2, LATTICE2, ZF_LANG, FILTER_1, WAYBEL_1; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, PRE_TOPC, STRUCT_0, WELLORD1, ORDERS_1, LATTICE3, QUANTAL1, ORDERS_3, YELLOW_0, GRCAT_1, YELLOW_1, WAYBEL_0, YELLOW_2; constructors TOPS_2, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, GRCAT_1; clusters STRUCT_0, RELSET_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, RELAT_1, FUNCT_2, PARTFUN1; requirements SUBSET, BOOLE; begin :: Preliminaries definition let L1,L2 be non empty 1-sorted, f be map of L1,L2; redefine attr f is one-to-one means :: WAYBEL_1:def 1 for x,y being Element of L1 st f.x = f.y holds x=y; end; theorem :: WAYBEL_1:1 for L being non empty 1-sorted, f being map of L,L st for x being Element of L holds f.x = x holds f = id L; definition let L1,L2 be non empty RelStr, f be map of L1,L2; redefine attr f is monotone means :: WAYBEL_1:def 2 for x,y being Element of L1 st x <= y holds f.x <= f.y; end; theorem :: WAYBEL_1:2 for L being antisymmetric transitive with_infima RelStr, x,y,z being Element of L st x <= y holds x "/\" z <= y "/\" z; theorem :: WAYBEL_1:3 for L being antisymmetric transitive with_suprema RelStr, x,y,z being Element of L st x <= y holds x "\/" z <= y "\/" z; theorem :: WAYBEL_1:4 for L being non empty lower-bounded antisymmetric RelStr for x being Element of L holds (L is with_infima implies Bottom L "/\" x = Bottom L) & (L is with_suprema reflexive transitive implies Bottom L "\/" x = x); theorem :: WAYBEL_1:5 for L being non empty upper-bounded antisymmetric RelStr for x being Element of L holds (L is with_infima transitive reflexive implies Top L "/\" x = x) & (L is with_suprema implies Top L "\/" x = Top L); definition let L be non empty RelStr; attr L is distributive means :: WAYBEL_1:def 3 for x,y,z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z); end; theorem :: WAYBEL_1:6 for L being LATTICE holds L is distributive iff for x,y,z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z); definition let X be set; cluster BoolePoset X -> distributive; end; definition let S be non empty RelStr, X be set; pred ex_min_of X,S means :: WAYBEL_1:def 4 ex_inf_of X,S & "/\"(X,S) in X; synonym X has_the_min_in S; pred ex_max_of X,S means :: WAYBEL_1:def 5 ex_sup_of X,S & "\/"(X,S) in X; synonym X has_the_max_in S; end; definition let S be non empty RelStr, s be Element of S, X be set; pred s is_minimum_of X means :: WAYBEL_1:def 6 ex_inf_of X,S & s = "/\"(X,S) & "/\"(X,S) in X; pred s is_maximum_of X means :: WAYBEL_1:def 7 ex_sup_of X,S & s = "\/"(X,S) & "\/"(X,S)in X; end; definition let L be RelStr; cluster id L -> isomorphic; end; definition let L1,L2 be RelStr; pred L1,L2 are_isomorphic means :: WAYBEL_1:def 8 ex f being map of L1,L2 st f is isomorphic; reflexivity; end; theorem :: WAYBEL_1:7 for L1,L2 be non empty RelStr st L1,L2 are_isomorphic holds L2,L1 are_isomorphic; theorem :: WAYBEL_1:8 for L1,L2,L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds L1,L3 are_isomorphic; begin :: Galois Connections definition let S,T be RelStr; mode Connection of S,T -> set means :: WAYBEL_1:def 9 ex g being map of S,T, d being map of T,S st it = [g,d]; end; definition let S,T be RelStr, g be map of S,T, d be map of T,S; redefine func [g,d] -> Connection of S,T; end; :: Definition 3.1 definition let S,T be non empty RelStr, gc be Connection of S,T; attr gc is Galois means :: WAYBEL_1:def 10 ex g being map of S,T, d being map of T,S st gc = [g,d] & g is monotone & d is monotone & for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s; end; theorem :: WAYBEL_1:9 for S,T being non empty Poset,g being map of S,T, d being map of T,S holds [g,d] is Galois iff g is monotone & d is monotone & for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s; :: Definition 3.1 definition let S,T be non empty RelStr, g be map of S,T; attr g is upper_adjoint means :: WAYBEL_1:def 11 ex d being map of T,S st [g,d] is Galois; synonym g has_a_lower_adjoint; end; :: Definition 3.1 definition let S,T be non empty RelStr, d be map of T,S; attr d is lower_adjoint means :: WAYBEL_1:def 12 ex g being map of S,T st [g,d] is Galois; synonym d has_an_upper_adjoint; end; theorem :: WAYBEL_1:10 for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds g is upper_adjoint & d is lower_adjoint; :: Theorem 3.2 (1) iff (2) theorem :: WAYBEL_1:11 for S,T being non empty Poset,g being map of S,T, d being map of T,S holds [g,d] is Galois iff g is monotone & for t being Element of T holds d.t is_minimum_of g"(uparrow t); :: Theorem 3.2 (1) iff (3) theorem :: WAYBEL_1:12 for S,T being non empty Poset,g being map of S,T, d being map of T,S holds [g,d] is Galois iff d is monotone & for s being Element of S holds g.s is_maximum_of d"(downarrow s); :: Theorem 3.3 (first part) theorem :: WAYBEL_1:13 for S,T being non empty Poset,g being map of S,T st g is upper_adjoint holds g is infs-preserving; definition let S,T be non empty Poset; cluster upper_adjoint -> infs-preserving map of S,T; end; :: Theorem 3.3 (second part) theorem :: WAYBEL_1:14 for S,T being non empty Poset, d being map of T,S st d is lower_adjoint holds d is sups-preserving; definition let S,T be non empty Poset; cluster lower_adjoint -> sups-preserving map of S,T; end; :: Theorem 3.4 theorem :: WAYBEL_1:15 for S,T being non empty Poset,g being map of S,T st S is complete & g is infs-preserving ex d being map of T,S st [g,d] is Galois & for t being Element of T holds d.t is_minimum_of g"(uparrow t); :: Theorem 3.4 (dual) theorem :: WAYBEL_1:16 for S,T being non empty Poset, d being map of T,S st T is complete & d is sups-preserving ex g being map of S,T st [g,d] is Galois & for s being Element of S holds g.s is_maximum_of d"(downarrow s); :: Corollary 3.5 (i) theorem :: WAYBEL_1:17 for S,T being non empty Poset, g being map of S,T st S is complete holds (g is infs-preserving iff g is monotone & g has_a_lower_adjoint); :: Corollary 3.5 (ii) theorem :: WAYBEL_1:18 for S,T being non empty Poset, d being map of T,S st T is complete holds d is sups-preserving iff d is monotone & d has_an_upper_adjoint; :: Theorem 3.6 (1) iff (2) theorem :: WAYBEL_1:19 for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds d*g <= id S & id T <= g*d; :: Theorem 3.6 (2) implies (1) theorem :: WAYBEL_1:20 for S,T being non empty Poset,g being map of S,T, d being map of T,S st g is monotone & d is monotone & d*g <= id S & id T <= g*d holds [g,d] is Galois; :: Theorem 3.6 (2) implies (3) theorem :: WAYBEL_1:21 for S,T being non empty Poset,g being map of S,T, d being map of T,S st g is monotone & d is monotone & d*g <= id S & id T <= g*d holds d = d*g*d & g = g*d*g; :: Theorem 3.6 (3) implies (4) theorem :: WAYBEL_1:22 for S,T being non empty RelStr, g being map of S,T, d being map of T,S st d = d*g*d & g = g*d*g holds g*d is idempotent & d*g is idempotent; :: Proposition 3.7 (1) implies (2) theorem :: WAYBEL_1:23 for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois & g is onto for t being Element of T holds d.t is_minimum_of g"{t}; :: Proposition 3.7 (2) implies (3) theorem :: WAYBEL_1:24 for S,T being non empty Poset,g being map of S,T, d being map of T,S st for t being Element of T holds d.t is_minimum_of g"{t} holds g*d = id T; :: Proposition 3.7 (3) implies (4) theorem :: WAYBEL_1:25 for L1,L2 being non empty 1-sorted, g1 being map of L1,L2, g2 being map of L2,L1 st g2*g1 = id L1 holds g1 is one-to-one & g2 is onto; :: Proposition 3.7 (4) iff (1) theorem :: WAYBEL_1:26 for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds g is onto iff d is one-to-one; :: Proposition 3.7 (1*) implies (2*) theorem :: WAYBEL_1:27 for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois & d is onto for s being Element of S holds g.s is_maximum_of d"{s}; :: Proposition 3.7 (2*) implies (3*) theorem :: WAYBEL_1:28 for S,T being non empty Poset,g being map of S,T, d being map of T,S st for s being Element of S holds g.s is_maximum_of d"{s} holds d*g = id S; :: Proposition 3.7 (1*) iff (4*) theorem :: WAYBEL_1:29 for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds g is one-to-one iff d is onto; :: Definition 3.8 (i) definition let L be non empty RelStr, p be map of L,L; attr p is projection means :: WAYBEL_1:def 13 p is idempotent monotone; synonym p is_a_projection_operator; end; definition let L be non empty RelStr; cluster id L -> projection; end; definition let L be non empty RelStr; cluster projection map of L,L; end; :: Definition 3.8 (ii) definition let L be non empty RelStr, c be map of L,L; attr c is closure means :: WAYBEL_1:def 14 c is projection & id(L) <= c; synonym c is_a_closure_operator; end; definition let L be non empty RelStr; cluster closure -> projection map of L,L; end; definition let L be non empty reflexive RelStr; cluster closure map of L,L; end; definition let L be non empty reflexive RelStr; cluster id L -> closure; end; :: Definition 3.8 (iii) definition let L be non empty RelStr, k be map of L,L; attr k is kernel means :: WAYBEL_1:def 15 k is projection & k <= id(L); synonym k is_a_kernel_operator; end; definition let L be non empty RelStr; cluster kernel -> projection map of L,L; end; definition let L be non empty reflexive RelStr; cluster kernel map of L,L; end; definition let L be non empty reflexive RelStr; cluster id L -> kernel; end; theorem :: WAYBEL_1:30 for L being non empty Poset, c being map of L,L, X being Subset of L st c is_a_closure_operator & ex_inf_of X,L & X c= rng c holds inf X = c.(inf X); theorem :: WAYBEL_1:31 for L being non empty Poset, k being map of L,L, X being Subset of L st k is_a_kernel_operator & ex_sup_of X,L & X c= rng k holds sup X = k.(sup X); definition let L1, L2 be non empty RelStr, g be map of L1,L2; func corestr(g) -> map of L1,Image g equals :: WAYBEL_1:def 16 (the carrier of Image g)|g; end; theorem :: WAYBEL_1:32 for L1, L2 being non empty RelStr,g being map of L1,L2 holds corestr g = g; definition let L1, L2 be non empty RelStr, g be map of L1,L2; cluster corestr g -> onto; end; theorem :: WAYBEL_1:33 for L1, L2 being non empty RelStr, g being map of L1,L2 st g is monotone holds corestr g is monotone; definition let L1, L2 be non empty RelStr, g be map of L1,L2; func inclusion(g) -> map of Image g,L2 equals :: WAYBEL_1:def 17 id Image g; end; theorem :: WAYBEL_1:34 for L1, L2 being non empty RelStr, g being map of L1,L2, s being Element of Image g holds (inclusion g).s = s; definition let L1, L2 be non empty RelStr, g be map of L1,L2; cluster inclusion g -> one-to-one monotone; end; theorem :: WAYBEL_1:35 for L being non empty RelStr, f being map of L,L holds (inclusion f)*(corestr f) = f; ::Theorem 3.10 (1) implies (2) theorem :: WAYBEL_1:36 for L being non empty Poset, f being map of L,L st f is idempotent holds (corestr f)*(inclusion f) = id(Image f); ::Theorem 3.10 (1) implies (3) theorem :: WAYBEL_1:37 for L being non empty Poset, f being map of L,L st f is_a_projection_operator ex T being non empty Poset, q being map of L,T, i being map of T,L st q is monotone & q is onto & i is monotone & i is one-to-one & f = i*q & id(T) = q*i; ::Theorem 3.10 (3) implies (1) theorem :: WAYBEL_1:38 for L being non empty Poset, f being map of L,L st (ex T being non empty Poset, q being map of L,T, i being map of T,L st q is monotone & i is monotone & f = i*q & id(T) = q*i) holds f is_a_projection_operator; ::Theorem 3.10 (1_1) implies (2_1) theorem :: WAYBEL_1:39 for L being non empty Poset, f being map of L,L st f is_a_closure_operator holds [inclusion f,corestr f] is Galois; ::Theorem 3.10 (2_1) implies (3_1) theorem :: WAYBEL_1:40 for L being non empty Poset, f being map of L,L st f is_a_closure_operator ex S being non empty Poset, g being map of S,L, d being map of L,S st [g,d] is Galois & f = g*d; ::Theorem 3.10 (3_1) implies (1_1) theorem :: WAYBEL_1:41 for L being non empty Poset, f being map of L,L st f is monotone & ex S being non empty Poset, g being map of S,L, d being map of L,S st [g,d] is Galois & f = g*d holds f is_a_closure_operator; ::Theorem 3.10 (1_2) implies (2_2) theorem :: WAYBEL_1:42 for L being non empty Poset, f being map of L,L st f is_a_kernel_operator holds [corestr f,inclusion f] is Galois; ::Theorem 3.10 (2_2) implies (3_2) theorem :: WAYBEL_1:43 for L being non empty Poset, f being map of L,L st f is_a_kernel_operator ex T being non empty Poset, g being map of L,T, d being map of T,L st [g,d] is Galois & f = d*g; ::Theorem 3.10 (3_2) implies (1_2) theorem :: WAYBEL_1:44 for L being non empty Poset, f being map of L,L st f is monotone & ex T being non empty Poset, g being map of L,T, d being map of T,L st [g,d] is Galois & f = d*g holds f is_a_kernel_operator; :: Lemma 3.11 (i) (part I) theorem :: WAYBEL_1:45 for L being non empty Poset, p being map of L,L st p is_a_projection_operator holds rng p = {c where c is Element of L: c <= p.c} /\ {k where k is Element of L: p.k <= k}; theorem :: WAYBEL_1:46 for L being non empty Poset, p being map of L,L st p is_a_projection_operator holds {c where c is Element of L: c <= p.c} is non empty Subset of L & {k where k is Element of L: p.k <= k} is non empty Subset of L; :: Lemma 3.11 (i) (part II) theorem :: WAYBEL_1:47 for L being non empty Poset, p being map of L,L st p is_a_projection_operator holds rng(p|{c where c is Element of L: c <= p.c}) = rng p & rng(p|{k where k is Element of L: p.k <= k}) = rng p; theorem :: WAYBEL_1:48 for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lc being non empty Subset of L, Lk being non empty Subset of L st Lc = {c where c is Element of L: c <= p.c} holds p|Lc is map of subrelstr Lc,subrelstr Lc; theorem :: WAYBEL_1:49 for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lk being non empty Subset of L st Lk = {k where k is Element of L: p.k <= k} holds p|Lk is map of subrelstr Lk,subrelstr Lk; :: Lemma 3.11 (i) (part IIIa) theorem :: WAYBEL_1:50 for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lc being non empty Subset of L st Lc = {c where c is Element of L: c <= p.c} for pc being map of subrelstr Lc,subrelstr Lc st pc = p|Lc holds pc is_a_closure_operator; :: Lemma 3.11 (i) (part IIIb) theorem :: WAYBEL_1:51 for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lk being non empty Subset of L st Lk = {k where k is Element of L: p.k <= k} for pk being map of subrelstr Lk,subrelstr Lk st pk = p|Lk holds pk is_a_kernel_operator; :: Lemma 3.11 (ii) (part I) theorem :: WAYBEL_1:52 for L being non empty Poset, p being map of L,L st p is monotone for Lc being Subset of L st Lc = {c where c is Element of L: c <= p.c} holds subrelstr Lc is sups-inheriting; :: Lemma 3.11 (ii) (part II) theorem :: WAYBEL_1:53 for L being non empty Poset, p being map of L,L st p is monotone for Lk being Subset of L st Lk = {k where k is Element of L: p.k <= k} holds subrelstr Lk is infs-inheriting; :: Lemma 3.11 (iii) (part I) theorem :: WAYBEL_1:54 for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lc being non empty Subset of L st Lc = {c where c is Element of L: c <= p.c} holds (p is infs-preserving implies subrelstr Lc is infs-inheriting & Image p is infs-inheriting) & (p is filtered-infs-preserving implies subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting); :: Lemma 3.11 (iii) (part II) theorem :: WAYBEL_1:55 for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lk being non empty Subset of L st Lk = {k where k is Element of L: p.k <= k} holds (p is sups-preserving implies subrelstr Lk is sups-inheriting & Image p is sups-inheriting) & (p is directed-sups-preserving implies subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting); :: Proposition 3.12 (i) theorem :: WAYBEL_1:56 for L being non empty Poset, p being map of L,L holds (p is_a_closure_operator implies Image p is infs-inheriting) & (p is_a_kernel_operator implies Image p is sups-inheriting); :: Proposition 3.12 (ii) theorem :: WAYBEL_1:57 for L being complete (non empty Poset), p being map of L,L st p is_a_projection_operator holds Image p is complete; :: Proposition 3.12 (iii) theorem :: WAYBEL_1:58 for L being non empty Poset, c being map of L,L st c is_a_closure_operator holds corestr c is sups-preserving & for X being Subset of L st X c= the carrier of Image c & ex_sup_of X,L holds ex_sup_of X,Image c & "\/"(X,Image c) = c.("\/"(X,L)); :: Proposition 3.12 (iv) theorem :: WAYBEL_1:59 for L being non empty Poset, k being map of L,L st k is_a_kernel_operator holds (corestr k) is infs-preserving & for X being Subset of L st X c= the carrier of Image k & ex_inf_of X,L holds ex_inf_of X,Image k & "/\"(X,Image k) = k.("/\"(X,L)); begin :: Heyting algebras :: Proposition 3.15 (i) theorem :: WAYBEL_1:60 for L being complete (non empty Poset) holds [IdsMap L,SupMap L] is Galois & SupMap L is sups-preserving; :: Proposition 3.15 (ii) theorem :: WAYBEL_1:61 for L being complete (non empty Poset) holds (IdsMap L)*(SupMap L) is_a_closure_operator & Image ((IdsMap L)*(SupMap L)),L are_isomorphic; definition let S be non empty RelStr; let x be Element of S; func x "/\" -> map of S,S means :: WAYBEL_1:def 18 for s being Element of S holds it.s = x"/\"s; end; theorem :: WAYBEL_1:62 for S being non empty RelStr, x,t being Element of S holds {s where s is Element of S: x"/\"s <= t} = (x "/\")"(downarrow t); theorem :: WAYBEL_1:63 for S being Semilattice, x be Element of S holds x "/\" is monotone; definition let S be Semilattice, x be Element of S; cluster x "/\" -> monotone; end; theorem :: WAYBEL_1:64 for S being non empty RelStr, x being Element of S, X being Subset of S holds (x "/\").:X = {x"/\"y where y is Element of S: y in X}; :: Lemma 3.16 (1) iff (2) theorem :: WAYBEL_1:65 for S being Semilattice holds (for x being Element of S holds x "/\" has_an_upper_adjoint) iff (for x,t being Element of S holds ex_max_of {s where s is Element of S: x"/\"s <= t},S); :: Lemma 3.16 (1) implies (3) theorem :: WAYBEL_1:66 for S being Semilattice st for x being Element of S holds x "/\" has_an_upper_adjoint for X being Subset of S st ex_sup_of X,S for x being Element of S holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S); :: Lemma 3.16 (1) iff (3) theorem :: WAYBEL_1:67 for S being complete (non empty Poset) holds (for x being Element of S holds x "/\" has_an_upper_adjoint) iff for X being Subset of S, x being Element of S holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S); :: Lemma 3.16 (3) implies (D) theorem :: WAYBEL_1:68 for S being LATTICE st for X being Subset of S st ex_sup_of X,S for x being Element of S holds x"/\"("\/"(X,S)) = "\/"({x"/\" y where y is Element of S: y in X},S) holds S is distributive; definition let H be non empty RelStr; attr H is Heyting means :: WAYBEL_1:def 19 H is LATTICE & for x being Element of H holds x "/\" has_an_upper_adjoint; synonym H is_a_Heyting_algebra; end; definition cluster Heyting -> with_infima with_suprema reflexive transitive antisymmetric (non empty RelStr); end; definition let H be non empty RelStr, a be Element of H; assume H is Heyting; func a => -> map of H,H means :: WAYBEL_1:def 20 [it,a "/\"] is Galois; end; theorem :: WAYBEL_1:69 for H being non empty RelStr st H is_a_Heyting_algebra holds H is distributive; definition cluster Heyting -> distributive (non empty RelStr); end; definition let H be non empty RelStr, a,y be Element of H; func a => y -> Element of H equals :: WAYBEL_1:def 21 (a=>).y; end; theorem :: WAYBEL_1:70 for H being non empty RelStr st H is_a_Heyting_algebra for x,a,y being Element of H holds x >= a "/\" y iff a => x >= y; theorem :: WAYBEL_1:71 for H being non empty RelStr st H is_a_Heyting_algebra holds H is upper-bounded; definition cluster Heyting -> upper-bounded (non empty RelStr); end; theorem :: WAYBEL_1:72 for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H holds Top H = a => b iff a <= b; theorem :: WAYBEL_1:73 for H being non empty RelStr st H is_a_Heyting_algebra for a being Element of H holds Top H = a => a; theorem :: WAYBEL_1:74 for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H st Top H = a => b & Top H = b => a holds a = b; theorem :: WAYBEL_1:75 for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H holds b <= (a => b); theorem :: WAYBEL_1:76 for H being non empty RelStr st H is_a_Heyting_algebra for a being Element of H holds Top H = a => Top H; theorem :: WAYBEL_1:77 for H being non empty RelStr st H is_a_Heyting_algebra for b being Element of H holds b = (Top H) => b; theorem :: WAYBEL_1:78 for H being non empty RelStr st H is_a_Heyting_algebra for a,b,c being Element of H st a <= b holds (b => c) <= (a => c); theorem :: WAYBEL_1:79 for H being non empty RelStr st H is_a_Heyting_algebra for a,b,c being Element of H st b <= c holds (a => b) <= (a => c); theorem :: WAYBEL_1:80 for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H holds a"/\"(a => b) = a"/\"b; theorem :: WAYBEL_1:81 for H being non empty RelStr st H is_a_Heyting_algebra for a,b,c being Element of H holds (a"\/"b)=> c = (a => c) "/\" (b => c); definition let H be non empty RelStr, a be Element of H; func 'not' a -> Element of H equals :: WAYBEL_1:def 22 a => Bottom H; end; theorem :: WAYBEL_1:82 for H being non empty RelStr st H is_a_Heyting_algebra & H is lower-bounded for a being Element of H holds 'not' a is_maximum_of {x where x is Element of H: a"/\"x = Bottom H} ; theorem :: WAYBEL_1:83 for H being non empty RelStr st H is_a_Heyting_algebra & H is lower-bounded holds 'not' Bottom H = Top H & 'not' Top H = Bottom H; :: Exercise 3.18 (i) theorem :: WAYBEL_1:84 for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' a >= b iff 'not' b >= a; :: Exercise 3.18 (ii) theorem :: WAYBEL_1:85 for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' a >= b iff a "/\" b = Bottom H; theorem :: WAYBEL_1:86 for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H st a <= b holds 'not' b <= 'not' a; theorem :: WAYBEL_1:87 for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b; theorem :: WAYBEL_1:88 for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' (a"/\"b) >= 'not' a"\/"'not' b; definition let L be non empty RelStr, x,y be Element of L; pred y is_a_complement_of x means :: WAYBEL_1:def 23 x "\/" y = Top L & x "/\" y = Bottom L; end; definition let L be non empty RelStr; attr L is complemented means :: WAYBEL_1:def 24 for x being Element of L ex y being Element of L st y is_a_complement_of x; end; definition let X be set; cluster BoolePoset X -> complemented; end; :: Exercise 3.19 theorem :: WAYBEL_1:89 for L being bounded LATTICE st L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not' x = x for x being Element of L holds 'not' x is_a_complement_of x; :: Exercise 3.19 (1) iff (2) theorem :: WAYBEL_1:90 for L being bounded LATTICE holds L is distributive complemented iff L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not' x = x; :: Definition 3.20 definition let B be non empty RelStr; attr B is Boolean means :: WAYBEL_1:def 25 B is LATTICE & B is bounded distributive complemented; synonym B is_a_Boolean_algebra; synonym B is_a_Boolean_lattice; end; definition cluster Boolean -> reflexive transitive antisymmetric with_infima with_suprema bounded distributive complemented (non empty RelStr); end; definition cluster reflexive transitive antisymmetric with_infima with_suprema bounded distributive complemented -> Boolean (non empty RelStr); end; definition cluster Boolean -> Heyting (non empty RelStr); end; definition cluster strict Boolean non empty LATTICE; end; definition cluster strict Heyting non empty LATTICE; end;

Back to top