P0 — Mathlib · SciLib

English

For every o that is a successor-limit ordinal, if P I o' holds for all o' < o, then P I o holds.

Русский

Для каждого o, являющегося предшественником предела-ординала, если P I o' верно для всех o' < o, то P I o верно.

LaTeX

$$$\\forall o : Ordinal, Order.IsSuccLimit o \\Rightarrow (\\forall o' : Ordinal, o' < o \\to P I o') \\to P I o$$$

Lean4

theorem P0 : P I 0 := fun _ C _ hsC ↦
  by
  have : C ⊆ {(fun _ ↦ false)} := fun c hc ↦ by ext x;
    exact Bool.eq_false_iff.mpr (fun ht ↦ (Ordinal.not_lt_zero (ord I x)) (hsC c hc x ht))
  rw [Set.subset_singleton_iff_eq] at this
  cases this
  · subst C
    exact linearIndependentEmpty
  · subst C
    exact linearIndependentSingleton

Похожие утверждения