mem_vonNeumann_succ_ranktheoremProved here from basic factspropext, Classical.choice, Quot.sound
mem_vonNeumann_succ_rankLean 4Proved here from basic factsFormally verified
/-- **Every set appears in the hierarchy**, at the stage after its rank: `x ∈ V_{rank(x)+1}`.Here `rank` is defined by ∈-recursion, `rank x = sup {rank y + 1 | y ∈ x}`, which is possiblebecause membership is well founded (the axiom of foundation); Mathlib shows `x ∈ V_α` iff`rank x < α` (`ZFSet.mem_vonNeumann`). -/theorem mem_vonNeumann_succ_rank (x : ZFSet) : x ∈ ZFSet.vonNeumann (Order.succ (ZFSet.rank x)) := ZFSet.mem_vonNeumann.mpr (Order.lt_succ (ZFSet.rank x))
exists_mem_vonNeumanntheoremApplies a library theorempropext, Classical.choice, Quot.sound
exists_mem_vonNeumannLean 4Applies a library theoremFormally verified
/-- `V = ⋃_α V_α`: every set lies in some `V_α`. This applies `ZFSet.exists_mem_vonNeumann`. -/theorem exists_mem_vonNeumann (x : ZFSet) : ∃ α, x ∈ ZFSet.vonNeumann α := ZFSet.exists_mem_vonNeumann x
not_mem_selftheoremProved here from basic factspropext, Classical.choice, Quot.sound
not_mem_selfLean 4Proved here from basic factsFormally verified
/-- No set is a member of itself. Proof via rank: `y ∈ x` implies `rank y < rank x`, so `x ∈ x`would give `rank x < rank x`. (Mathlib proves the same as `ZFSet.mem_irrefl`.) -/theorem not_mem_self (x : ZFSet) : x ∉ x := fun h => lt_irrefl _ (ZFSet.rank_lt_of_mem h)
no_mem_two_cycletheoremProved here from basic factspropext, Classical.choice, Quot.sound
no_mem_two_cycleLean 4Proved here from basic factsFormally verified
/-- There are no membership 2-cycles `x ∈ y ∈ x`: their ranks would satisfy`rank x < rank y < rank x`. The same argument excludes cycles of every length. -/theorem no_mem_two_cycle (x y : ZFSet) : ¬ (x ∈ y ∧ y ∈ x) := fun ⟨hxy, hyx⟩ => lt_irrefl _ ((ZFSet.rank_lt_of_mem hxy).trans (ZFSet.rank_lt_of_mem hyx))
koenig_power_coftheoremApplies a library theorempropext, Classical.choice, Quot.sound
koenig_power_cofLean 4Applies a library theoremFormally verified
/-- **König's theorem**, in the form `κ < κ^cf(κ)` for infinite `κ`: an infinite cardinal issmaller than the number of `cf(κ)`-sequences from it. (It follows from `∑ᵢ κᵢ < ∏ᵢ λᵢ` when`κᵢ < λᵢ`, Mathlib's `Cardinal.sum_lt_prod`.) This applies `Cardinal.lt_power_cof_ord`; here`c.ord.cof` is the cofinality of the initial ordinal of `c`. -/theorem koenig_power_cof {κ : Cardinal} (hκ : ℵ₀ ≤ κ) : κ < κ ^ κ.ord.cof := lt_power_cof_ord hκ
two_power_aleph0_ne_aleph_omegatheoremProved here from basic factspropext, Classical.choice, Quot.sound
two_power_aleph0_ne_aleph_omegaLean 4Proved here from basic factsFormally verified
/-- **The continuum is not `ℵ_ω`.** The cardinal `ℵ_ω = sup {ℵₙ | n < ω}` has cofinality `ℵ₀`,while König gives `cf(2^ℵ₀) > ℵ₀`. Here `ℵ_ω` is `ℵ_ ω` and its initial ordinal is `ω_ ω`, whosecofinality equals that of `ω` (Mathlib's `Ordinal.cof_omega`). -/theorem two_power_aleph0_ne_aleph_omega : (2 : Cardinal) ^ ℵ₀ ≠ ℵ_ ω := by intro h have hk := koenig_cof_two_power (le_refl ℵ₀) rw [h, ord_aleph, cof_omega isSuccLimit_omega0, cof_omega0] at hk exact lt_irrefl _ hk
/-- The **generalised continuum hypothesis**: `2^κ = κ⁺` for every infinite cardinal `κ`, where`κ⁺ = Order.succ κ` is the next cardinal. Gödel showed that it holds in `L`, so it is consistentwith ZFC (if ZF is); Cohen showed that its negation is consistent too. -/def GCH : Prop := ∀ κ : Cardinal.{u}, ℵ₀ ≤ κ → 2 ^ κ = Order.succ κ
/-- There are no membership 2-cycles `x ∈ y ∈ x`.Hint: `ZFSet.rank_lt_of_mem : y ∈ x → rank y < rank x`; chain two of these and use `lt_irrefl`. -/theorem no_mem_two_cycle (x y : ZFSet) : ¬ (x ∈ y ∧ y ∈ x) := by sorry
Show the compiled solution
no_mem_two_cycleLean 4Proved here from basic factsFormally verified
/-- There are no membership 2-cycles `x ∈ y ∈ x`: their ranks would satisfy`rank x < rank y < rank x`. The same argument excludes cycles of every length. -/theorem no_mem_two_cycle (x y : ZFSet) : ¬ (x ∈ y ∧ y ∈ x) := fun ⟨hxy, hyx⟩ => lt_irrefl _ ((ZFSet.rank_lt_of_mem hxy).trans (ZFSet.rank_lt_of_mem hyx))