Grace/Cumulus/Set/Core.g17

Open in Workbench Download source

Imports

Hierarchy

Declarations

• Nonempty predicate
• Disjoint predicate
• Subset.transitive theorem derivation
• Subset.antisymmetric theorem derivation
• empty.subset theorem derivation
• union2.subset theorem derivation
• union2.subset_left theorem derivation
• union2.subset_right theorem derivation
• union.contains theorem derivation
• union.subset theorem derivation
• intersection.subset_right theorem derivation
• intersection.greatest theorem derivation
• difference.subset_left theorem derivation
• powerset.membership_iff theorem derivation
• powerset.monotone theorem derivation
• Nonempty.singleton theorem derivation
• Nonempty.ne_empty theorem derivation
• Nonempty.of_ne_empty theorem derivation
• Nonempty.iff_ne_empty theorem derivation
• Disjoint.symmetric theorem derivation
• singleton.ne_empty theorem derivation

Source

1-- Foundational set mathematics2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Set.Core8import Hierarchy910-- The public root of Cumulus set theory: extensional mathematics,11-- classes, relations, Foundation, ordinals, rank, and the cumulative hierarchy.12predicate Nonempty (A : Set) := ∃ x, x ∈ A13predicate Disjoint (A B : Set) := A ∩ B = ∅1415theorem Subset.transitive (A B C : Set)16  requires hAB : A ⊆ B17  requires hBC : B ⊆ C18  shows (A ⊆ C)19proof20  simp2122theorem Subset.antisymmetric (A B : Set)23  requires hAB : A ⊆ B24  requires hBA : B ⊆ A25  shows A = B26proof27  ext y28  simp2930theorem empty.subset (A : Set)31  shows (∅ ⊆ A)32proof33  simp3435theorem union2.subset (A B C : Set)36  requires hA : A ⊆ C37  requires hB : B ⊆ C38  shows (A ∪ B ⊆ C)39proof40  simp4142theorem union2.subset_left (A B : Set)43  shows (A ⊆ A ∪ B)44proof45  simp4647theorem union2.subset_right (A B : Set)48  shows (B ⊆ A ∪ B)49proof50  simp5152theorem union.contains (x A S : Set)53  requires hA : A ∈ S54  requires hx : x ∈ A55  shows x ∈ ⋃(S)56proof57  simp [set.union]5859theorem union.subset (S B : Set)60  requires h : ∀ A ∈ S, (A ⊆ B)61  shows (⋃(S) ⊆ B)62proof63  intros x hx64  simp [set.union] at hx65  obtain ⟨A, hAS, hxA⟩ := hx66  exact h with A, hAS, x, hxA6768theorem intersection.subset_right (A B : Set)69  shows (A ∩ B ⊆ B)70proof71  simp7273theorem intersection.greatest (A B C : Set)74  requires hA : C ⊆ A75  requires hB : C ⊆ B76  shows (C ⊆ A ∩ B)77proof78  simp7980theorem difference.subset_left (A B : Set)81  shows (A ∖ B ⊆ A)82proof83  simp8485theorem powerset.membership_iff (A B : Set)86  shows A ∈ 𝒫(B) ↔ (A ⊆ B)87proof88  simp8990theorem powerset.monotone (A B : Set)91  requires h : A ⊆ B92  shows (𝒫(A) ⊆ 𝒫(B))93proof94  simp [Subset, set.powerset]9596theorem Nonempty.singleton (x : Set)97  shows Nonempty({x})98proof99  simp [Nonempty]100101theorem Nonempty.ne_empty (A : Set)102  requires inhabited : Nonempty(A)103  shows A ≠ ∅104proof105  intro equal106  obtain ⟨x, member⟩ := inhabited107  rw equal at member108  exact set.empty with member109110-- The converse needs only classical logic and extensionality.111theorem Nonempty.of_ne_empty (A : Set)112  requires different : A ≠ ∅113  shows Nonempty(A)114proof115  by_contra absent116  apply different117  ext x118  constructor119  . intro member120    exfalso121    apply absent122    unfold Nonempty123    refine ⟨x, member⟩124  . intro member125    exfalso126    exact set.empty with member127128theorem Nonempty.iff_ne_empty (A : Set)129  shows Nonempty(A) ↔ A ≠ ∅130proof131  simp [Nonempty.ne_empty, Nonempty.of_ne_empty]132133theorem Disjoint.symmetric (A B : Set)134  requires h : Disjoint(A, B)135  shows Disjoint(B, A)136proof137  unfold Disjoint at h138  unfold Disjoint139  rwa intersection.commutative140141theorem singleton.ne_empty (x : Set)142  shows {x} ≠ ∅143proof144  intro singletonEmpty145  have self := singleton.self at x146  rw singletonEmpty at self147  simp148149