Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### Ideals

**by****Grzegorz Bancerek**- Received October 24, 1994
- MML identifier: FILTER_2

- [ Mizar article, MML identifier index ]

environ vocabulary BINOP_1, RELAT_1, FUNCT_1, LATTICE2, LATTICES, SUBSET_1, LATTICE4, FILTER_0, BOOLE, NAT_LAT, ZF_LANG, FILTER_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, FUNCT_1, DOMAIN_1, BINOP_1, LATTICES, NAT_LAT, FILTER_0, LATTICE2, MCART_1, RELSET_1, LATTICE4; constructors DOMAIN_1, BINOP_1, NAT_LAT, FILTER_0, LATTICE2, LATTICE4, XBOOLE_0; clusters LATTICES, FILTER_0, NAT_LAT, LATTICE2, FUNCT_1, STRUCT_0, RLSUB_2, RELSET_1, LATTICE4, SUBSET_1, XBOOLE_0, ZFMISC_1; requirements SUBSET, BOOLE; begin :: Some Properties of the Restriction of Binary Operations theorem :: FILTER_2:1 for D being non empty set, S being non empty Subset of D, f being BinOp of D, g being BinOp of S st g = f|[:S,S:] holds (f is commutative implies g is commutative) & (f is idempotent implies g is idempotent) & (f is associative implies g is associative); theorem :: FILTER_2:2 for D being non empty set, S being non empty Subset of D, f being BinOp of D, g being BinOp of S for d being Element of D, d' being Element of S st g = f|[:S,S:] & d' = d holds (d is_a_left_unity_wrt f implies d' is_a_left_unity_wrt g) & (d is_a_right_unity_wrt f implies d' is_a_right_unity_wrt g) & (d is_a_unity_wrt f implies d' is_a_unity_wrt g); theorem :: FILTER_2:3 for D being non empty set, S being non empty Subset of D, f1,f2 being BinOp of D, g1,g2 being BinOp of S st g1 = f1|[:S,S:] & g2 = f2|[:S,S:] holds (f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2) & (f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2); theorem :: FILTER_2:4 for D being non empty set, S being non empty Subset of D, f1,f2 being BinOp of D, g1,g2 being BinOp of S st g1 = f1|[:S,S:] & g2 = f2|[:S,S:] holds f1 is_distributive_wrt f2 implies g1 is_distributive_wrt g2; theorem :: FILTER_2:5 for D being non empty set, S being non empty Subset of D, f1,f2 being BinOp of D, g1,g2 being BinOp of S st g1 = f1|[:S,S:] & g2 = f2|[:S,S:] holds f1 absorbs f2 implies g1 absorbs g2; begin :: Closed Subsets of a Lattice definition let D be non empty set, X1,X2 be Subset of D; redefine pred X1 = X2 means :: FILTER_2:def 1 for x being Element of D holds x in X1 iff x in X2; end; reserve L for Lattice, p,q,r for Element of L, p',q',r' for Element of L.:, x,y for set; theorem :: FILTER_2:6 for L1,L2 being LattStr st the LattStr of L1 = the LattStr of L2 holds L1.: = L2.:; theorem :: FILTER_2:7 L.:.: = the LattStr of L; theorem :: FILTER_2:8 for L1,L2 being non empty LattStr st the LattStr of L1 = the LattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1 = b2 holds a1"\/"b1 = a2"\/"b2 & a1"/\"b1 = a2"/\"b2 & (a1 [= b1 iff a2 [= b2); theorem :: FILTER_2:9 for L1,L2 being 0_Lattice st the LattStr of L1 = the LattStr of L2 holds Bottom L1 = Bottom L2; theorem :: FILTER_2:10 for L1,L2 being 1_Lattice st the LattStr of L1 = the LattStr of L2 holds Top L1 = Top L2; theorem :: FILTER_2:11 for L1,L2 being C_Lattice st the LattStr of L1 = the LattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2; theorem :: FILTER_2:12 for L1,L2 being B_Lattice st the LattStr of L1 = the LattStr of L2 for a being Element of L1, b being Element of L2 st a = b holds a` = b`; theorem :: FILTER_2:13 for X being Subset of L st for p,q holds p in X & q in X iff p"/\"q in X holds X is ClosedSubset of L; theorem :: FILTER_2:14 for X being Subset of L st for p,q holds p in X & q in X iff p"\/"q in X holds X is ClosedSubset of L; definition let L; redefine mode Filter of L -> non empty ClosedSubset of L; end; definition let L; redefine func <.L.) -> Filter of L; let p be Element of L; func <.p.) -> Filter of L; end; definition let L; let D be non empty Subset of L; redefine func <.D.) -> Filter of L; end; definition let L be D_Lattice; let F1,F2 be Filter of L; redefine func F1 "/\" F2 -> Filter of L; end; definition let L; canceled; mode Ideal of L -> non empty ClosedSubset of L means :: FILTER_2:def 3 p in it & q in it iff p "\/" q in it; end; theorem :: FILTER_2:15 for X being non empty Subset of L st for p,q holds p in X & q in X iff p "\/" q in X holds X is Ideal of L; theorem :: FILTER_2:16 for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2 for x st x is Filter of L1 holds x is Filter of L2; theorem :: FILTER_2:17 for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2 for x st x is Ideal of L1 holds x is Ideal of L2; definition let L,p; func p.: -> Element of L.: equals :: FILTER_2:def 4 p; end; definition let L; let p be Element of L.:; func .:p -> Element of L equals :: FILTER_2:def 5 p; end; theorem :: FILTER_2:18 .:(p.:) = p & ( .:p').: = p'; theorem :: FILTER_2:19 p"/\"q = p.:"\/"q.: & p"\/"q = p.:"/\"q.: & p'"/\"q' = .:p'"\/".: q' & p'"\/"q' = .:p' "/\".:q'; theorem :: FILTER_2:20 (p [= q iff q.: [= p.:) & (p' [= q' iff .:q' [= .:p'); theorem :: FILTER_2:21 x is Ideal of L iff x is Filter of L.:; definition let L; let X be Subset of L; func X.: -> Subset of L.: equals :: FILTER_2:def 6 X; end; definition let L; let X be Subset of L.:; func .:X -> Subset of L equals :: FILTER_2:def 7 X; end; definition let L; let D be non empty Subset of L; cluster D.: -> non empty; end; definition let L; let D be non empty Subset of L.:; cluster .:D -> non empty; end; definition let L; let S be ClosedSubset of L; redefine func S.: -> ClosedSubset of L.:; end; definition let L; let S be non empty ClosedSubset of L; redefine func S.: -> non empty ClosedSubset of L.:; end; definition let L; let S be ClosedSubset of L.:; redefine func .:S -> ClosedSubset of L; end; definition let L; let S be non empty ClosedSubset of L.:; redefine func .:S -> non empty ClosedSubset of L; end; definition let L; let F be Filter of L; redefine func F.: -> Ideal of L.:; end; definition let L; let F be Filter of L.:; redefine func .:F -> Ideal of L; end; definition let L; let I be Ideal of L; redefine func I.: -> Filter of L.:; end; definition let L; let I be Ideal of L.:; redefine func .:I -> Filter of L; end; theorem :: FILTER_2:22 for D being non empty Subset of L holds D is Ideal of L iff (for p,q st p in D & q in D holds p "\/" q in D) & for p,q st p in D & q [= p holds q in D; reserve I,J for Ideal of L, F for Filter of L; theorem :: FILTER_2:23 p in I implies p"/\"q in I & q"/\"p in I; theorem :: FILTER_2:24 ex p st p in I; theorem :: FILTER_2:25 L is lower-bounded implies Bottom L in I; theorem :: FILTER_2:26 L is lower-bounded implies {Bottom L} is Ideal of L; theorem :: FILTER_2:27 {p} is Ideal of L implies L is lower-bounded; begin :: Ideals Generated by Subsets of a Lattice theorem :: FILTER_2:28 the carrier of L is Ideal of L; definition let L; func (.L.> -> Ideal of L equals :: FILTER_2:def 8 the carrier of L; end; definition let L,p; func (.p.> -> Ideal of L equals :: FILTER_2:def 9 { q : q [= p }; end; theorem :: FILTER_2:29 q in (.p.> iff q [= p; theorem :: FILTER_2:30 (.p.> = <.p.:.) & (.p.:.> = <.p.); theorem :: FILTER_2:31 p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.>; theorem :: FILTER_2:32 L is upper-bounded implies (.L.> = (.Top L.>; definition let L,I; pred I is_max-ideal means :: FILTER_2:def 10 I <> the carrier of L & for J st I c= J & J <> the carrier of L holds I = J; end; theorem :: FILTER_2:33 I is_max-ideal iff I.: is_ultrafilter; theorem :: FILTER_2:34 L is upper-bounded implies for I st I <> the carrier of L ex J st I c= J & J is_max-ideal; theorem :: FILTER_2:35 (ex r st p "\/" r <> p) implies (.p.> <> the carrier of L; theorem :: FILTER_2:36 L is upper-bounded & p <> Top L implies ex I st p in I & I is_max-ideal; reserve D for non empty Subset of L, D' for non empty Subset of L.:; definition let L,D; func (.D.> -> Ideal of L means :: FILTER_2:def 11 D c= it & for I st D c= I holds it c= I; end; theorem :: FILTER_2:37 <.D.:.) = (.D.> & <.D.) = (.D.:.> & <..:D'.) = (.D'.> & <.D'.) = (..: D'.>; theorem :: FILTER_2:38 (.I.> = I; reserve D1,D2 for non empty Subset of L, D1',D2' for non empty Subset of L.:; theorem :: FILTER_2:39 (D1 c= D2 implies (.D1.> c= (.D2.>) & (.(.D.>.> c= (.D.>; theorem :: FILTER_2:40 p in D implies (.p.> c= (.D.>; theorem :: FILTER_2:41 D = {p} implies (.D.> = (.p.>; theorem :: FILTER_2:42 L is upper-bounded & Top L in D implies (.D.> = (.L.> & (.D.> = the carrier of L; theorem :: FILTER_2:43 L is upper-bounded & Top L in I implies I = (.L.> & I = the carrier of L; definition let L,I; attr I is prime means :: FILTER_2:def 12 p "/\" q in I iff p in I or q in I; end; theorem :: FILTER_2:44 I is prime iff I.: is prime; definition let L,D1,D2; func D1 "\/" D2 -> Subset of L equals :: FILTER_2:def 13 { p"\/"q : p in D1 & q in D2 }; end; definition let L,D1,D2; cluster D1 "\/" D2 -> non empty; end; theorem :: FILTER_2:45 D1 "\/" D2 = D1.: "/\" D2.: & D1.: "\/" D2.: = D1 "/\" D2 & D1' "\/" D2' = .:D1' "/\" .:D2' & .:D1' "\/" .:D2' = D1' "/\" D2'; theorem :: FILTER_2:46 p in D1 & q in D2 implies p"\/"q in D1 "\/" D2 & q"\/"p in D1 "\/" D2; theorem :: FILTER_2:47 x in D1 "\/" D2 implies ex p,q st x = p"\/"q & p in D1 & q in D2; theorem :: FILTER_2:48 D1 "\/" D2 = D2 "\/" D1; definition let L be D_Lattice; let I1,I2 be Ideal of L; redefine func I1 "\/" I2 -> Ideal of L; end; theorem :: FILTER_2:49 (.D1 \/ D2.> = (.(.D1.> \/ D2.> & (.D1 \/ D2.> = (.D1 \/ (.D2.>.>; theorem :: FILTER_2:50 (.I \/ J.> = { r : ex p,q st r [= p"\/"q & p in I & q in J }; theorem :: FILTER_2:51 I c= I "\/" J & J c= I "\/" J; theorem :: FILTER_2:52 (.I \/ J.> = (.I "\/" J.>; reserve B for B_Lattice, I_B,J_B for Ideal of B, a,b for Element of B; theorem :: FILTER_2:53 L is C_Lattice iff L.: is C_Lattice; theorem :: FILTER_2:54 L is B_Lattice iff L.: is B_Lattice; definition let B be B_Lattice; cluster B.: -> Boolean Lattice-like; end; reserve a' for Element of (B qua Lattice).:; theorem :: FILTER_2:55 a.:` = a` & ( .:a')` = a'`; theorem :: FILTER_2:56 (.I_B \/ J_B.> = I_B "\/" J_B; theorem :: FILTER_2:57 I_B is_max-ideal iff I_B <> the carrier of B & for a holds a in I_B or a` in I_B; theorem :: FILTER_2:58 I_B <> (.B.> & I_B is prime iff I_B is_max-ideal; theorem :: FILTER_2:59 I_B is_max-ideal implies for a holds a in I_B iff not a` in I_B; theorem :: FILTER_2:60 a <> b implies ex I_B st I_B is_max-ideal & (a in I_B & not b in I_B or not a in I_B & b in I_B); reserve P for non empty ClosedSubset of L, o1,o2 for BinOp of P; theorem :: FILTER_2:61 (the L_join of L)|[:P,P:] is BinOp of P & (the L_meet of L)|[:P,P:] is BinOp of P; theorem :: FILTER_2:62 o1 = (the L_join of L)|[:P,P:] & o2 = (the L_meet of L)|[:P,P:] implies o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1; definition let L,p,q; assume p [= q; func [#p,q#] -> non empty ClosedSubset of L equals :: FILTER_2:def 14 {r: p [= r & r [= q}; end; theorem :: FILTER_2:63 p [= q implies (r in [#p,q#] iff p [= r & r [= q); theorem :: FILTER_2:64 p [= q implies p in [#p,q#] & q in [#p,q#]; theorem :: FILTER_2:65 [#p,p#] = {p}; theorem :: FILTER_2:66 L is upper-bounded implies <.p.) = [#p,Top L#]; theorem :: FILTER_2:67 L is lower-bounded implies (.p.> = [#Bottom L,p#]; theorem :: FILTER_2:68 for L1,L2 being Lattice for F1 being Filter of L1, F2 being Filter of L2 st the LattStr of L1 = the LattStr of L2 & F1 = F2 holds latt F1 = latt F2; begin :: Sublattices definition let L; redefine mode SubLattice of L means :: FILTER_2:def 15 ex P,o1,o2 st o1 = (the L_join of L)|[:P,P:] & o2 = (the L_meet of L)|[:P,P:] & the LattStr of it = LattStr (#P, o1, o2#); synonym Sublattice of L; end; theorem :: FILTER_2:69 for K being Sublattice of L, a being Element of K holds a is Element of L; definition let L,P; func latt (L,P) -> Sublattice of L means :: FILTER_2:def 16 ex o1,o2 st o1 = (the L_join of L)|[:P,P:] & o2 = (the L_meet of L)|[:P,P:] & it = LattStr (#P, o1, o2#); end; definition let L,P; cluster latt (L,P) -> strict; end; definition let L; let l be Sublattice of L; redefine func l.: -> strict Sublattice of L.:; end; theorem :: FILTER_2:70 latt F = latt (L,F); theorem :: FILTER_2:71 latt (L,P) = (latt (L.:,P.:)).:; theorem :: FILTER_2:72 latt (L,(.L.>) = the LattStr of L & latt (L,<.L.)) = the LattStr of L; theorem :: FILTER_2:73 the carrier of latt (L,P) = P & the L_join of latt (L,P) = (the L_join of L)|[:P,P:] & the L_meet of latt (L,P) = (the L_meet of L)|[:P,P:]; theorem :: FILTER_2:74 for p,q for p',q' being Element of latt (L,P) st p = p' & q = q' holds p"\/"q = p'"\/"q' & p"/\"q = p'"/\"q'; theorem :: FILTER_2:75 for p,q for p',q' being Element of latt (L,P) st p = p' & q = q' holds p [= q iff p' [= q'; theorem :: FILTER_2:76 L is lower-bounded implies latt (L,I) is lower-bounded; theorem :: FILTER_2:77 L is modular implies latt (L,P) is modular; theorem :: FILTER_2:78 L is distributive implies latt (L,P) is distributive; theorem :: FILTER_2:79 L is implicative & p [= q implies latt (L,[#p,q#]) is implicative; theorem :: FILTER_2:80 latt (L,(.p.>) is upper-bounded; theorem :: FILTER_2:81 Top latt (L,(.p.>) = p; theorem :: FILTER_2:82 L is lower-bounded implies latt (L,(.p.>) is lower-bounded & Bottom latt (L,(.p.>) = Bottom L; theorem :: FILTER_2:83 L is lower-bounded implies latt (L,(.p.>) is bounded; theorem :: FILTER_2:84 p [= q implies latt (L,[#p,q#]) is bounded & Top latt (L,[#p,q#]) = q & Bottom latt (L,[#p,q#]) = p; theorem :: FILTER_2:85 L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice; theorem :: FILTER_2:86 L is C_Lattice & L is modular & p [= q implies latt (L,[#p,q#]) is C_Lattice; theorem :: FILTER_2:87 L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice;

Back to top