Grace/Cumulus/Set/Ordinal/Basic.g17

Open in Workbench Download source

Imports

Core · Family

Declarations

• Ordinal.not_member_self theorem derivation
• Ordinal.member_subset theorem derivation
• Ordinal.not_member_of_subset theorem derivation
• Ordinal.subset_or_member theorem derivation
• Ordinal.member_iff_proper_subset theorem derivation
• Ordinal.subset_iff_member_next theorem derivation
• Ordinal.member_iff_next_subset theorem derivation
• next.injective theorem derivation
• next.not_member_self theorem derivation
• next.member_iff theorem derivation
• Ordinal.union_upper theorem derivation
• Ordinal.union_least theorem derivation
• Ordinal.union_next theorem derivation
• Ordinal.least theorem derivation
• Ordinal.intersection_least theorem derivation
• ordinalsWithin def
• ordinalsWithin.ordinal theorem derivation
• Ordinal.no_set_of_all theorem derivation

Source

1-- The order of the ordinals: membership as a strict order, successors,2-- inclusion, least elements, and the Burali-Forti collection3-- 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.Ordinal.Basic9import Core10import Family1112theorem Ordinal.not_member_self (α : Set)13  shows ¬(α ∈ α)14proof15  exact membership.irreflexive1617theorem Ordinal.member_subset (α β : Set)18  requires hBeta : β ∈ Ordinal19  requires h : α ∈ β20  shows α ⊆ β21proof22  have transitive := Ordinal.transitive with hBeta23  exact transitive with α, h2425theorem Ordinal.not_member_of_subset (α β : Set)26  requires h : β ⊆ α27  shows ¬(α ∈ β)28proof29  intro member30  exact Ordinal.not_member_self with (h with α, member)3132theorem Ordinal.subset_or_member (α β : Set)33  requires hAlpha : α ∈ Ordinal34  requires hBeta : β ∈ Ordinal35  shows α ⊆ β ∨ β ∈ α36proof37  have cases := Ordinal.trichotomy with hAlpha, β, hBeta38  cases cases with less | rest39  . left40    exact Ordinal.member_subset with hBeta, less41  . cases rest with equal | greater42    . left43      rw equal44      exact Subset.reflexive45    . right46      exact greater4748theorem Ordinal.member_iff_proper_subset (α β : Set)49  requires hAlpha : α ∈ Ordinal50  requires hBeta : β ∈ Ordinal51  shows α ∈ β ↔ α ⊆ β ∧ α ≠ β52proof53  constructor54  . intro h55    constructor56    . exact Ordinal.member_subset with hBeta, h57    . intro equal58      rw equal at h59      exact Ordinal.not_member_self with h60  . intro h61    have cases := Ordinal.trichotomy with hAlpha, β, hBeta62    cases cases with less | rest63    . exact less64    . cases rest with equal | greater65      . exfalso66        exact h.right with equal67      . exfalso68        exact Ordinal.not_member_of_subset with h.left, greater6970theorem Ordinal.subset_iff_member_next (α β : Set)71  requires hAlpha : α ∈ Ordinal72  requires hBeta : β ∈ Ordinal73  shows α ⊆ β ↔ α ∈ next(β)74proof75  constructor76  . intro h77    exact Ordinal.subset_bound with hAlpha, hBeta, h78  . intro h79    simp [next.membership] at h80    cases h with less | equal81    . exact Ordinal.member_subset with hBeta, less82    . rw equal83      exact Subset.reflexive8485theorem Ordinal.member_iff_next_subset (α β : Set)86  requires hAlpha : α ∈ Ordinal87  requires hBeta : β ∈ Ordinal88  shows α ∈ β ↔ next(α) ⊆ β89proof90  constructor91  . intros h x hx92    simp [next.membership] at hx93    cases hx with less | equal94    . exact Ordinal.member_subset at α, β with hBeta, h, x, less95    . rw equal96      exact h97  . intro h98    exact h with α, (next.contains at α)99100theorem next.injective (α β : Set)101  requires hAlpha : α ∈ Ordinal102  requires hBeta : β ∈ Ordinal103  requires h : next(α) = next(β)104  shows α = β105proof106  have alphaIn : α ∈ next(β)107    rw ← h108    exact next.contains109  have betaIn : β ∈ next(α)110    rw h111    exact next.contains112  simp [next.membership] at alphaIn113  simp [next.membership] at betaIn114  cases alphaIn with less | equal115  . cases betaIn with lessBack | equalBack116    . exfalso117      have included := Ordinal.member_subset with hAlpha, lessBack118      exact Ordinal.not_member_of_subset with included, less119    . symm120      exact equalBack121  . exact equal122123theorem next.not_member_self (α : Set)124  requires hAlpha : α ∈ Ordinal125  shows ¬(next(α) ∈ α)126proof127  intro h128  have included := Ordinal.member_subset with hAlpha, h129  exact Ordinal.not_member_self with (included with α, (next.contains at α))130131theorem next.member_iff (α β : Set)132  requires hAlpha : α ∈ Ordinal133  requires hBeta : β ∈ Ordinal134  shows next(α) ∈ next(β) ↔ α ∈ β135proof136  constructor137  . intro h138    have included := Ordinal.subset_iff_member_next.backward with (Ordinal.next with hAlpha), hBeta, h139    exact included with α, (next.contains at α)140  . intro h141    apply Ordinal.subset_iff_member_next.forward with (Ordinal.next with hAlpha), hBeta142    exact Ordinal.member_iff_next_subset.forward with hAlpha, hBeta, h143144theorem Ordinal.union_upper (A α : Set)145  requires h : α ∈ A146  shows α ⊆ ⋃(A)147proof148  exact union.subset_of_member with h149150theorem Ordinal.union_least (A β : Set)151  requires h : ∀ α ∈ A, α ⊆ β152  shows ⋃(A) ⊆ β153proof154  exact union.subset with h155156theorem Ordinal.union_next (α : Set)157  requires hAlpha : α ∈ Ordinal158  shows ⋃(next(α)) = α159proof160  apply Subset.antisymmetric161  . apply union.subset162    intros β hβ163    simp [next.membership] at hβ164    cases hβ with less | equal165    . exact Ordinal.member_subset with hAlpha, less166    . rw equal167      exact Subset.reflexive168  . exact union.subset_of_member with (next.contains at α)169170theorem Ordinal.least (S : Set)171  requires ordinals : ∀ α ∈ S, α ∈ Ordinal172  requires nonempty : S ≠ ∅173  shows ∃ m ∈ S, ∀ α ∈ S, m ⊆ α174proof175  have found := membership.wellFounded at S176  have within : ∀ x ∈ S, x ∈ S177    intros x hx178    exact hx179  obtain ⟨m, hm, minimal⟩ := found with S, within, nonempty180  witness m181  constructor182  . exact hm183  . intros α hα184    have cases := Ordinal.subset_or_member with (ordinals with m, hm), (ordinals with α, hα)185    cases cases with included | greater186    . exact included187    . exfalso188      exact minimal with α, greater, hα189190-- The least element of a nonempty set of ordinals is its intersection.191theorem Ordinal.intersection_least (S : Set)192  requires ordinals : ∀ α ∈ S, α ∈ Ordinal193  requires nonempty : S ≠ ∅194  shows ⋂(S) ∈ S ∧ (∀ α ∈ S, ⋂(S) ⊆ α)195proof196  obtain ⟨m, hm, least⟩ := Ordinal.least with ordinals, nonempty197  have inhabited : Nonempty(S) := ⟨m, hm⟩198  have equal : ⋂(S) = m199    apply Subset.antisymmetric200    . exact familyIntersection.subset_of_member with hm201    . exact familyIntersection.greatest with inhabited, least202  constructor203  . rw equal204    exact hm205  . intros α hα206    rw equal207    exact least with α, hα208209-- The ordinals among the members of X.210def ordinalsWithin (X : Set) : Set := { α ∈ X | α ∈ Ordinal }211212theorem ordinalsWithin.ordinal (X : Set)213  requires h : ∀ α, α ∈ Ordinal → α ∈ X214  shows ordinalsWithin(X) ∈ Ordinal215proof216  have transitive : Transitive(ordinalsWithin(X))217    intros α hα218    simp [ordinalsWithin.membership] at hα219    intros β hβ220    have ordinal := Ordinal.member with hα.right, hβ221    simp [ordinalsWithin.membership]222  simp [Ordinal]223224theorem Ordinal.no_set_of_all225  shows ¬(∃ X, ∀ α, α ∈ Ordinal → α ∈ X)226proof227  intro h228  obtain ⟨X, hX⟩ := h229  have ordinal := ordinalsWithin.ordinal with hX230  have selfMember : ordinalsWithin(X) ∈ ordinalsWithin(X) by simp [ordinalsWithin.membership]231  exact Ordinal.not_member_self with selfMember232