Grace/Cumulus/Set/Family.g17

Open in Workbench Download source

Imports

Powerset

Declarations

Source

1-- Families of sets: intersections of families, complements within a2-- carrier, and the De Morgan laws between them3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Set.Family9import Powerset1011-- The intersection of a family is carved out of its union, so it is a set12-- for every family and the empty family's intersection is empty.13def familyIntersection (S : Set) : Set := { x ∈ ⋃(S) | ∀ A ∈ S, x ∈ A }14notation prefix 90 "⋂" => familyIntersection1516-- The complement of A within a carrier E.17def complement (E A : Set) : Set := E ∖ A1819-- The family of complements of the members of S within E.20def complements (E S : Set) : Set := { E ∖ A | A ∈ S }2122theorem familyIntersection.membership_of_nonempty (x S : Set)23  requires nonempty : Nonempty(S)24  shows x ∈ ⋂(S) ↔ ∀ A ∈ S, x ∈ A25proof26  constructor27  . intro h28    simp [familyIntersection] at h29    exact h.right30  . intro h31    obtain ⟨B, hB⟩ := nonempty32    simp [familyIntersection]33    constructor34    . exact union.contains with hB, (h with B, hB)35    . exact h3637theorem familyIntersection.subset_of_member (A S : Set)38  requires h : A ∈ S39  shows ⋂(S) ⊆ A40proof41  intros x hx42  simp [familyIntersection] at hx43  exact hx.right with A, h4445theorem familyIntersection.subset_union (S : Set)46  shows ⋂(S) ⊆ ⋃(S)47proof48  intros x hx49  simp [familyIntersection] at hx50  exact hx.left5152theorem familyIntersection.empty53  shows ⋂(∅) = ∅54proof55  apply Subset.empty_iff.forward56  have included := familyIntersection.subset_union at ∅57  rwa union.empty at included5859theorem familyIntersection.greatest (Z S : Set)60  requires nonempty : Nonempty(S)61  requires h : ∀ A ∈ S, Z ⊆ A62  shows Z ⊆ ⋂(S)63proof64  intros x hx65  apply familyIntersection.membership_of_nonempty.backward with nonempty66  intros A hA67  exact h with A, hA, x, hx6869theorem familyIntersection.antitone (S T : Set)70  requires nonempty : Nonempty(S)71  requires h : S ⊆ T72  shows ⋂(T) ⊆ ⋂(S)73proof74  apply familyIntersection.greatest with nonempty75  intros A hA76  exact familyIntersection.subset_of_member with (h with A, hA)7778theorem familyIntersection.singleton (A : Set)79  shows ⋂({A}) = A80proof81  apply Subset.antisymmetric82  . exact familyIntersection.subset_of_member with (singleton.self at A)83  . apply familyIntersection.greatest with (Nonempty.singleton at A)84    intros B hB85    simp [singleton.membership] at hB86    rw hB87    exact Subset.reflexive8889theorem familyIntersection.pair (A B : Set)90  shows ⋂({A, B}) = A ∩ B91proof92  apply Subset.antisymmetric93  . apply Subset.intersection_iff.backward94    constructor95    . exact familyIntersection.subset_of_member with (pair.left at A, B)96    . exact familyIntersection.subset_of_member with (pair.right at A, B)97  . have nonempty : Nonempty({A, B}) := ⟨A, (pair.left at A, B)⟩98    apply familyIntersection.greatest with nonempty99    intros C hC100    simp at hC101    cases hC with hA | hB102    . rw hA103      exact intersection.subset_left104    . rw hB105      exact intersection.subset_right106107theorem familyIntersection.union2 (S T : Set)108  requires nonemptyS : Nonempty(S)109  requires nonemptyT : Nonempty(T)110  shows ⋂(S ∪ T) = ⋂(S) ∩ ⋂(T)111proof112  apply Subset.antisymmetric113  . apply Subset.intersection_iff.backward114    constructor115    . exact familyIntersection.antitone with nonemptyS, (union2.subset_left at S, T)116    . exact familyIntersection.antitone with nonemptyT, (union2.subset_right at S, T)117  . obtain ⟨B, hB⟩ := nonemptyS118    have nonempty : Nonempty(S ∪ T) := ⟨B, (union2.subset_left at S, T with B, hB)⟩119    apply familyIntersection.greatest with nonempty120    intros A hA121    simp [union2.membership] at hA122    cases hA with hS | hT123    . exact Subset.transitive with (intersection.subset_left at ⋂(S), ⋂(T)), (familyIntersection.subset_of_member with hS)124    . exact Subset.transitive with (intersection.subset_right at ⋂(S), ⋂(T)), (familyIntersection.subset_of_member with hT)125126-- Complements within a carrier127128theorem complement.membership (x E A : Set)129  shows x ∈ complement(E, A) ↔ x ∈ E ∧ ¬(x ∈ A)130proof131  simp [complement, difference.membership]132133theorem complement.subset (E A : Set)134  shows complement(E, A) ⊆ E135proof136  simp [complement]137138theorem complement.union2 (E A : Set)139  requires h : A ⊆ E140  shows A ∪ complement(E, A) = E141proof142  simp [complement]143  ext y144  simp145146theorem complement.intersection (E A : Set)147  shows A ∩ complement(E, A) = ∅148proof149  ext y150  simp [complement]151152theorem complement.complement (E A : Set)153  requires h : A ⊆ E154  shows complement(E, complement(E, A)) = A155proof156  simp [complement]157  ext y158  simp159160theorem complement.empty (E : Set)161  shows complement(E, ∅) = E162proof163  simp [complement]164  exact difference.empty165166theorem complement.self (E : Set)167  shows complement(E, E) = ∅168proof169  simp [complement]170  exact difference.self171172theorem complement.antitone (E A B : Set)173  requires h : A ⊆ B174  shows complement(E, B) ⊆ complement(E, A)175proof176  intros x hx177  simp [complement.membership] at hx178  simp [complement.membership]179180theorem complement.subset_iff (E A B : Set)181  requires hA : A ⊆ E182  requires hB : B ⊆ E183  shows A ⊆ B ↔ complement(E, B) ⊆ complement(E, A)184proof185  constructor186  . intro h187    exact complement.antitone with h188  . intros h x hx189    by_contra absent190    have inE : x ∈ E := hA with x, hx191    have member : x ∈ complement(E, B) by simp [complement.membership, inE, absent]192    have inComplement : x ∈ complement(E, A) := h with x, member193    simp [complement.membership] at inComplement194195theorem complement.injective (E A B : Set)196  requires hA : A ⊆ E197  requires hB : B ⊆ E198  requires h : complement(E, A) = complement(E, B)199  shows A = B200proof201  have double := complement.complement with hA202  rw [← double, h]203  exact complement.complement with hB204205theorem complement.union2_distrib (E A B : Set)206  shows complement(E, A ∪ B) = complement(E, A) ∩ complement(E, B)207proof208  simp [complement]209  exact difference.union2210211theorem complement.intersection_distrib (E A B : Set)212  shows complement(E, A ∩ B) = complement(E, A) ∪ complement(E, B)213proof214  simp [complement]215  exact difference.intersection216217theorem complement.disjoint_iff (E A B : Set)218  requires hA : A ⊆ E219  shows Disjoint(A, B) ↔ A ⊆ complement(E, B)220proof221  constructor222  . intro h223    have absent := Disjoint.iff.forward with h224    intros x hx225    simp [complement.membership]226  . intro h227    apply Disjoint.iff.backward228    intros x hx229    have member : x ∈ complement(E, B) := h with x, hx230    simp [complement.membership] at member231    exact member.right232233-- De Morgan laws for families234235theorem complements.union (E S : Set)236  requires nonempty : Nonempty(S)237  shows complement(E, ⋃(S)) = ⋂(complements(E, S))238proof239  obtain ⟨C, hC⟩ := nonempty240  have nonemptyComplements : Nonempty(complements(E, S))241    witness E ∖ C242    apply complements.membership.backward243    witness C244    constructor245    . exact hC246    . rfl247  ext x248  constructor249  . intro hx250    simp [complement.membership] at hx251    apply familyIntersection.membership_of_nonempty.backward with nonemptyComplements252    intros B hB253    obtain ⟨A, hA, shape⟩ := complements.membership.forward with hB254    rw ← shape255    simp [difference.membership]256    constructor257    . exact hx.left258    . intro inA259      exact hx.right with (union.contains with hA, inA)260  . intro hx261    have everywhere := familyIntersection.membership_of_nonempty.forward with nonemptyComplements, hx262    have inFirst : x ∈ E ∖ C263      apply everywhere264      apply complements.membership.backward265      witness C266      constructor267      . exact hC268      . rfl269    simp [difference.membership] at inFirst270    simp [complement.membership]271    constructor272    . exact inFirst.left273    . intro inUnion274      simp [set.union] at inUnion275      obtain ⟨A, hA, inA⟩ := inUnion276      have inComplement : x ∈ E ∖ A277        apply everywhere278        apply complements.membership.backward279        witness A280        constructor281        . exact hA282        . rfl283      simp [difference.membership] at inComplement284285theorem complements.intersection (E S : Set)286  requires nonempty : Nonempty(S)287  shows complement(E, ⋂(S)) = ⋃(complements(E, S))288proof289  ext x290  constructor291  . intro hx292    simp [complement.membership] at hx293    have notEverywhere : ¬(∀ A ∈ S, x ∈ A)294      intro everywhere295      exact hx.right with (familyIntersection.membership_of_nonempty.backward with nonempty, everywhere)296    by_contra absent297    apply notEverywhere298    intros A hA299    by_contra outside300    apply absent301    have inComplement : x ∈ E ∖ A by simp [difference.membership, hx.left, outside]302    have member : E ∖ A ∈ complements(E, S)303      apply complements.membership.backward304      witness A305      constructor306      . exact hA307      . rfl308    exact union.contains with member, inComplement309  . intro hx310    simp [set.union] at hx311    obtain ⟨B, hB, inB⟩ := hx312    obtain ⟨A, hA, shape⟩ := complements.membership.forward with hB313    rw ← shape at inB314    simp [difference.membership] at inB315    simp [complement.membership]316    constructor317    . exact inB.left318    . intro inIntersection319      have inA : x ∈ A := familyIntersection.subset_of_member with hA, x, inIntersection320      exact inB.right with inA321