Grace/Cumulus/Set/Powerset.g17

Open in Workbench Download source

Imports

Algebra

Declarations

Source

1-- Singletons, pairs, power sets, unions of families, and products:2-- the basic set constructions and their laws3-- 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.Powerset9import Algebra1011-- Singletons and pairs1213theorem singleton.subset_iff (x A : Set)14  shows {x} ⊆ A ↔ x ∈ A15proof16  constructor17  . intro h18    exact h with x, (singleton.self at x)19  . intros h y hy20    simp [singleton.membership] at hy21    rwa hy2223theorem singleton.injective (x y : Set)24  requires h : {x} = {y}25  shows x = y26proof27  have member : x ∈ {y}28    rw ← h29    exact singleton.self30  simpa [singleton.membership] using member3132theorem singleton.eq_iff (x y : Set)33  shows {x} = {y} ↔ x = y34proof35  constructor36  . intro h37    exact singleton.injective with h38  . intro h39    rw h40    rfl4142theorem subset_singleton.cases (Y x : Set)43  requires h : Y ⊆ {x}44  shows Y = ∅ ∨ Y = {x}45proof46  by_contra neither47  have nonempty : Y ≠ ∅48    intro hY49    apply neither50    left51    exact hY52  obtain ⟨y, hy⟩ := Nonempty.of_ne_empty with nonempty53  have hyx : y ∈ {x} := h with y, hy54  simp [singleton.membership] at hyx55  apply neither56  right57  ext z58  constructor59  . intro hz60    exact h with z, hz61  . intro hz62    simp [singleton.membership] at hz63    rwa [hz, ← hyx]6465theorem pair.commutative (x y : Set)66  shows {x, y} = {y, x}67proof68  ext z69  simp7071theorem pair.eq_union2 (x y : Set)72  shows {x, y} = {x} ∪ {y}73proof74  ext z75  simp7677theorem pair.self (x : Set)78  shows {x, x} = {x}79proof80  ext z81  simp8283theorem pair.subset_iff (x y A : Set)84  shows {x, y} ⊆ A ↔ x ∈ A ∧ y ∈ A85proof86  constructor87  . intro h88    constructor89    . exact h with x, (pair.left at x, y)90    . exact h with y, (pair.right at x, y)91  . intros h z hz92    simp at hz93    cases hz with hx | hy94    . rw hx95      exact h.left96    . rw hy97      exact h.right9899theorem singleton.subset_pair (x y : Set)100  shows {x} ⊆ {x, y}101proof102  simp103104theorem pair.cancel_right (a b c : Set)105  requires h : {a, c} = {b, c}106  shows a = b107proof108  have member : a ∈ {b, c}109    rw ← h110    exact pair.left111  simp at member112  cases member with hab | hac113  . exact hab114  . have other : b ∈ {a, c}115      rw h116      exact pair.left117    simp at other118    cases other with hba | hbc119    . symm120      exact hba121    . rw [hac, hbc]122      rfl123124theorem singleton.eq_pair_iff (x a b : Set)125  shows {x} = {a, b} ↔ x = a ∧ x = b126proof127  constructor128  . intro h129    have inA : a ∈ {x}130      rw h131      exact pair.left132    have inB : b ∈ {x}133      rw h134      exact pair.right135    simp [singleton.membership] at inA136    simp [singleton.membership] at inB137    constructor138    . symm139      exact inA140    . symm141      exact inB142  . intro h143    rw [← h.left, ← h.right]144    symm145    exact pair.self146147theorem difference.singleton_membership (z A x : Set)148  shows z ∈ A ∖ {x} ↔ z ∈ A ∧ z ≠ x149proof150  simp [difference.membership, singleton.membership]151152theorem difference.singleton_of_absent (A x : Set)153  requires h : ¬(x ∈ A)154  shows A ∖ {x} = A155proof156  ext z157  simp [difference.membership, singleton.membership]158159-- Power sets160161theorem powerset.self (A : Set)162  shows A ∈ 𝒫(A)163proof164  exact powerset.membership_iff.backward with (Subset.reflexive at A)165166theorem powerset.empty_member (A : Set)167  shows ∅ ∈ 𝒫(A)168proof169  exact powerset.membership_iff.backward with (empty.subset at A)170171theorem powerset.subset_iff (A B : Set)172  shows 𝒫(A) ⊆ 𝒫(B) ↔ A ⊆ B173proof174  constructor175  . intro h176    have member : A ∈ 𝒫(B) := h with A, (powerset.self at A)177    simpa [powerset.membership_iff] using member178  . intro h179    exact powerset.monotone with h180181theorem powerset.injective (A B : Set)182  requires h : 𝒫(A) = 𝒫(B)183  shows A = B184proof185  apply Subset.antisymmetric186  . exact powerset.subset_iff.forward with (Subset.of_eq with h)187  . symm at h188    exact powerset.subset_iff.forward with (Subset.of_eq with h)189190theorem powerset.intersection (A B : Set)191  shows 𝒫(A ∩ B) = 𝒫(A) ∩ 𝒫(B)192proof193  ext z194  simp [powerset.membership_iff, intersection.membership, Subset.intersection_iff]195196theorem powerset.union2_subset (A B : Set)197  shows 𝒫(A) ∪ 𝒫(B) ⊆ 𝒫(A ∪ B)198proof199  intros z hz200  simp [union2.membership, powerset.membership_iff] at hz201  simp [powerset.membership_iff]202203theorem powerset.union_subset (A : Set)204  shows A ⊆ 𝒫(⋃(A))205proof206  intros z hz207  simp [powerset.membership_iff]208  intros w hw209  exact union.contains with hz, hw210211theorem powerset.union (A : Set)212  shows ⋃(𝒫(A)) = A213proof214  apply Subset.antisymmetric215  . apply union.subset216    intros z hz217    simpa [powerset.membership_iff] using hz218  . intros z hz219    exact union.contains with (powerset.self at A), hz220221-- Unions of families222223theorem union.membership (x S : Set)224  shows x ∈ ⋃(S) ↔ ∃ A ∈ S, x ∈ A225proof226  simp [set.union]227228theorem union.subset_of_member (A S : Set)229  requires h : A ∈ S230  shows A ⊆ ⋃(S)231proof232  intros z hz233  exact union.contains with h, hz234235theorem union.monotone (S T : Set)236  requires h : S ⊆ T237  shows ⋃(S) ⊆ ⋃(T)238proof239  apply union.subset240  intros A hA241  exact union.subset_of_member with (h with A, hA)242243theorem union.pair (A B : Set)244  shows ⋃({A, B}) = A ∪ B245proof246  apply Subset.antisymmetric247  . apply union.subset248    intros C hC249    simp at hC250    cases hC with hA | hB251    . rw hA252      exact union2.subset_left253    . rw hB254      exact union2.subset_right255  . intros z hz256    simp [union2.membership] at hz257    cases hz with hA | hB258    . exact union.contains with (pair.left at A, B), hA259    . exact union.contains with (pair.right at A, B), hB260261theorem union.union2 (S T : Set)262  shows ⋃(S ∪ T) = ⋃(S) ∪ ⋃(T)263proof264  apply Subset.antisymmetric265  . apply union.subset266    intros A hA267    simp [union2.membership] at hA268    cases hA with hS | hT269    . exact union2.subset_of_subset_left with (union.subset_of_member with hS)270    . exact union2.subset_of_subset_right with (union.subset_of_member with hT)271  . apply union2.subset272    . exact union.monotone with (union2.subset_left at S, T)273    . exact union.monotone with (union2.subset_right at S, T)274275theorem union.intersection_subset (S T : Set)276  shows ⋃(S ∩ T) ⊆ ⋃(S) ∩ ⋃(T)277proof278  apply Subset.intersection_iff.backward279  constructor280  . exact union.monotone with (intersection.subset_left at S, T)281  . exact union.monotone with (intersection.subset_right at S, T)282283theorem union.eq_empty_iff (S : Set)284  shows ⋃(S) = ∅ ↔ ∀ A ∈ S, A = ∅285proof286  constructor287  . intros h A hA288    apply Subset.empty_iff.forward289    rw ← h290    exact union.subset_of_member with hA291  . intro h292    apply Subset.empty_iff.forward293    apply union.subset294    intros A hA295    have empty : A = ∅ := h with A, hA296    rw empty297    exact Subset.reflexive298299theorem union.subset_powerset (S A : Set)300  requires h : S ⊆ 𝒫(A)301  shows ⋃(S) ⊆ A302proof303  apply union.subset304  intros B hB305  have member : B ∈ 𝒫(A) := h with B, hB306  simpa [powerset.membership_iff] using member307308-- Products309310theorem product.pair_membership (x y A B : Set)311  shows (x, y) ∈ A × B ↔ x ∈ A ∧ y ∈ B312proof313  constructor314  . intro h315    simp [product.membership] at h316    obtain ⟨bound, a, ha, b, hb, equation⟩ := h317    obtain ⟨hxa, hyb⟩ := orderedPair.injective with equation318    rw [hxa, hyb]319    constructor320    . exact ha321    . exact hb322  . intro h323    exact product.pair with h.left, h.right324325theorem product.left_empty (B : Set)326  shows ∅ × B = ∅327proof328  ext p329  constructor330  . intro hp331    simp [product.membership] at hp332  . intro hp333    exact empty.subset at ∅ × B with p, hp334335theorem product.right_empty (A : Set)336  shows A × ∅ = ∅337proof338  ext p339  constructor340  . intro hp341    simp [product.membership] at hp342  . intro hp343    exact empty.subset at A × ∅ with p, hp344345theorem product.eq_empty_iff (A B : Set)346  shows A × B = ∅ ↔ A = ∅ ∨ B = ∅347proof348  constructor349  . intro h350    by_contra neither351    have hA : A ≠ ∅352      intro hA353      apply neither354      left355      exact hA356    have hB : B ≠ ∅357      intro hB358      apply neither359      right360      exact hB361    obtain ⟨a, ha⟩ := Nonempty.of_ne_empty with hA362    obtain ⟨b, hb⟩ := Nonempty.of_ne_empty with hB363    have member : (a, b) ∈ A × B := product.pair with ha, hb364    rw h at member365    simpa using member366  . intro h367    cases h with hA | hB368    . rw hA369      exact product.left_empty370    . rw hB371      exact product.right_empty372373theorem product.union2_left (A B C : Set)374  shows (A ∪ B) × C = (A × C) ∪ (B × C)375proof376  ext p377  constructor378  . intro hp379    simp [product.membership] at hp380    obtain ⟨bound, a, ha, c, hc, equation⟩ := hp381    rw equation382    simp [union2.membership] at ha383    simp [union2.membership]384    cases ha with hA | hB385    . left386      exact product.pair with hA, hc387    . right388      exact product.pair with hB, hc389  . intro hp390    simp [union2.membership] at hp391    cases hp with hAC | hBC392    . exact product.monotone at A, C, A ∪ B, C with (union2.subset_left at A, B), (Subset.reflexive at C), p, hAC393    . exact product.monotone at B, C, A ∪ B, C with (union2.subset_right at A, B), (Subset.reflexive at C), p, hBC394395theorem product.union2_right (A B C : Set)396  shows A × (B ∪ C) = (A × B) ∪ (A × C)397proof398  ext p399  constructor400  . intro hp401    simp [product.membership] at hp402    obtain ⟨bound, a, ha, b, hb, equation⟩ := hp403    rw equation404    simp [union2.membership] at hb405    simp [union2.membership]406    cases hb with hB | hC407    . left408      exact product.pair with ha, hB409    . right410      exact product.pair with ha, hC411  . intro hp412    simp [union2.membership] at hp413    cases hp with hAB | hAC414    . exact product.monotone at A, B, A, B ∪ C with (Subset.reflexive at A), (union2.subset_left at B, C), p, hAB415    . exact product.monotone at A, C, A, B ∪ C with (Subset.reflexive at A), (union2.subset_right at B, C), p, hAC416417theorem product.difference_left (A B C : Set)418  shows (A ∖ B) × C = (A × C) ∖ (B × C)419proof420  ext p421  constructor422  . intro hp423    obtain ⟨_, a, ha, c, hc, rfl⟩ := product.membership.forward with hp424    obtain ⟨inA, notInB⟩ := difference.membership.forward with ha425    apply difference.membership.backward426    constructor427    . exact product.pair with inA, hc428    . intro inB429      have coordinates := product.pair_membership.forward with inB430      exact notInB with coordinates.left431  . intro hp432    obtain ⟨inAC, notInBC⟩ := difference.membership.forward with hp433    obtain ⟨_, a, ha, c, hc, rfl⟩ := product.membership.forward with inAC434    have notInB : ¬a ∈ B435      intro inB436      exact notInBC with (product.pair with inB, hc)437    have inDifference := difference.membership.backward with ⟨ha, notInB⟩438    exact product.pair with inDifference, hc439440theorem product.symmetricDifference_left (A B C : Set)441  shows (A △ B) × C = (A × C) △ (B × C)442proof443  unfold symmetricDifference444  rw [product.union2_left, product.difference_left, product.difference_left]445  rfl446447theorem product.intersection (A B C D : Set)448  shows (A ∩ B) × (C ∩ D) = (A × C) ∩ (B × D)449proof450  ext p451  constructor452  . intro hp453    simp [product.membership] at hp454    obtain ⟨bound, a, ha, c, hc, equation⟩ := hp455    rw equation456    simp [intersection.membership] at ha457    simp [intersection.membership] at hc458    simp [intersection.membership]459    constructor460    . exact product.pair with ha.left, hc.left461    . exact product.pair with ha.right, hc.right462  . intro hp463    simp [intersection.membership] at hp464    obtain ⟨hAC, hBD⟩ := hp465    simp [product.membership] at hAC466    obtain ⟨bound, a, ha, c, hc, equation⟩ := hAC467    rw equation at hBD468    rw equation469    have coordinates := product.pair_membership.forward with hBD470    apply product.pair471    . simp [intersection.membership]472    . simp [intersection.membership]473474-- Products with disjoint factors are disjoint.475theorem product.disjoint_of_right (A B C D : Set)476  requires disjoint : Disjoint(B, D)477  shows Disjoint(A × B, C × D)478proof479  have separated := Disjoint.iff.forward with disjoint480  apply Disjoint.iff.backward481  intros p hp hp2482  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp483  rw shape at hp2484  have coordinates := product.pair_membership.forward with hp2485  exact separated with y, hy, coordinates.right486487theorem product.disjoint_of_left (A B C D : Set)488  requires disjoint : Disjoint(A, C)489  shows Disjoint(A × B, C × D)490proof491  have separated := Disjoint.iff.forward with disjoint492  apply Disjoint.iff.backward493  intros p hp hp2494  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp495  rw shape at hp2496  have coordinates := product.pair_membership.forward with hp2497  exact separated with x, hx, coordinates.left498499theorem product.subset_of_nonempty (A B C D : Set)500  requires nonempty : Nonempty(A × B)501  requires h : A × B ⊆ C × D502  shows A ⊆ C ∧ B ⊆ D503proof504  obtain ⟨p, hp⟩ := nonempty505  simp [product.membership] at hp506  obtain ⟨bound, a, ha, b, hb, equation⟩ := hp507  constructor508  . intros x hx509    have member : (x, b) ∈ C × D := h with (x, b), (product.pair with hx, hb)510    have coordinates := product.pair_membership.forward with member511    exact coordinates.left512  . intros y hy513    have member : (a, y) ∈ C × D := h with (a, y), (product.pair with ha, hy)514    have coordinates := product.pair_membership.forward with member515    exact coordinates.right516517theorem product.singleton (x y : Set)518  shows {x} × {y} = {(x, y)}519proof520  ext p521  constructor522  . intro hp523    simp [product.membership] at hp524    obtain ⟨bound, a, ha, b, hb, equation⟩ := hp525    simp [singleton.membership] at ha526    simp [singleton.membership] at hb527    rw [equation, ha, hb]528    exact singleton.self529  . intro hp530    simp [singleton.membership] at hp531    rw hp532    exact product.pair with (singleton.self at x), (singleton.self at y)533