English
Cof o equals 1 if and only if o is a successor; cof(o)=1 ⇔ ∃ a, o = succ a.
Русский
Cof o равна 1 тогда и только тогда, когда o — это переходный порядок; cof(o)=1 ⇔ ∃ a, o = succ a.
LaTeX
$$$$\operatorname{cof}(o)=1 \iff \exists a,\ o=\operatorname{succ} a.$$$$
Lean4
@[simp]
theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a :=
⟨inductionOn o fun α r _ z => by
rcases cof_eq r with ⟨S, hl, e⟩; rw [z] at e
obtain ⟨a⟩ := mk_ne_zero_iff.1 (by rw [e]; exact one_ne_zero)
refine
⟨typein r a,
Eq.symm <| Quotient.sound ⟨RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ fun x y => ?_) fun x => ?_⟩⟩
· apply Sum.rec <;> [exact Subtype.val; exact fun _ => a]
· rcases x with (x | ⟨⟨⟨⟩⟩⟩) <;> rcases y with (y | ⟨⟨⟨⟩⟩⟩) <;> simp [Subrel, Order.Preimage, EmptyRelation]
exact x.2
· suffices r x a ∨ ∃ _ : PUnit.{u}, ↑a = x by
convert this
dsimp [RelEmbedding.ofMonotone]; simp
rcases trichotomous_of r x a with (h | h | h)
· exact Or.inl h
· exact Or.inr ⟨PUnit.unit, h.symm⟩
· rcases hl x with ⟨a', aS, hn⟩
refine absurd h ?_
convert hn
change (a : α) = ↑(⟨a', aS⟩ : S)
have := le_one_iff_subsingleton.1 (le_of_eq e)
congr!,
fun ⟨a, e⟩ => by simp [e]⟩
