Grace/Cumulus/Set/Basic.g17

Open in Workbench Download source

Imports

None

Declarations

• singleton def
• union2 def
• intersection def
• difference def
• Subset predicate
• pair.left theorem derivation
• pair.right theorem derivation
• pair.cancel_left theorem derivation
• singleton.self theorem derivation
• union2.left theorem derivation
• union.empty theorem derivation
• union.singleton theorem derivation
• intersection.commutative theorem derivation
• Subset.reflexive theorem derivation
• intersection.subset_left theorem derivation
• intersection.idempotent theorem derivation

Source

1-- Basic set theory2-- 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.Basic89namespace Set1011def singleton (x : Set) : Set := pair(x, x)12def union2 (A B : Set) : Set := ⋃(pair(A, B))13def intersection (A B : Set) : Set := { x ∈ A | x ∈ B }14def difference (A B : Set) : Set := { x ∈ A | ¬x ∈ B }15predicate Subset (A B : Set) := ∀ x ∈ A, x ∈ B16notation infix 50 "⊆" => Subset17notation infixl 60 "∪" => union218notation infixl 65 "∩" => intersection19notation infixl 65 "∖" => difference2021theorem pair.left (x y : Set)22  shows x ∈ {x, y}23proof24  simp2526theorem pair.right (x y : Set)27  shows y ∈ {x, y}28proof29  simp3031theorem pair.cancel_left (a b c : Set)32  requires h : {a, b} = {a, c}33  shows b = c34proof35  have hb := pair.right at a, b36  rw h at hb37  simp [pair.membership] at hb38  cases hb with hba | hbc39  have hc := pair.right at a, c40  rw ← h at hc41  simp [pair.membership] at hc42  cases hc with hca | hcb43  simp44  simp45  exact hbc4647theorem singleton.self (x : Set)48  shows x ∈ {x}49proof50  simp [singleton, pair.membership]5152theorem union2.left (x A B : Set)53  requires x ∈ A54  shows x ∈ A ∪ B55proof56  simp [union2, set.union, pair.membership]5758theorem union.empty59  shows ⋃(∅) = ∅60proof61  ext y62  simp [set.union, set.empty]6364theorem union.singleton (A : Set)65  shows ⋃({A}) = A66proof67  ext y68  simp [set.union, singleton, pair.membership]6970theorem intersection.commutative (A B : Set)71  shows A ∩ B = B ∩ A72proof73  ext y74  simp7576theorem Subset.reflexive (A : Set)77  shows (A ⊆ A)78proof79  simp8081theorem intersection.subset_left (A B : Set)82  shows (A ∩ B ⊆ A)83proof84  simp8586theorem intersection.idempotent (A : Set)87  shows A ∩ A = A88proof89  ext y90  simp9192end Set9394export open Grace.Cumulus.Set.Basic.Set95