cof_eq' — Mathlib

English

Let (α,r) be a well-ordered set with type r, and suppose type r is a succ-limit ordinal. Then there exists a subset S ⊆ α such that for every a ∈ α there is b ∈ S with a < b, and |S| = cof(type r).

Русский

Пусть (α,r) — хорошо упорядоченное множество, чьё порядковое отображение имеет succ-предел; тогда существует множество S ⊆ α, такое что для каждого a ∈ α найдётся b ∈ S с a < b, и |S| = cof(type r).

LaTeX

$$$$ \exists S \subseteq \alpha,\ (\forall a \in \alpha,\ \exists b \in S,\ r\ a\ b) \land |S| = \operatorname{cof}(\operatorname{type}(r)). $$$$

Lean4

theorem cof_eq' (r : α → α → Prop) [IsWellOrder α r] (h : IsSuccLimit (type r)) :
    ∃ S : Set α, (∀ a, ∃ b ∈ S, r a b) ∧ #S = cof (type r) :=
  let ⟨S, H, e⟩ := cof_eq r
  ⟨S, fun a =>
    let a' := enum r ⟨_, h.succ_lt (typein_lt_type r a)⟩
    let ⟨b, h, ab⟩ := H a'
    ⟨b, h,
      (IsOrderConnected.conn a b a' <|
            (typein_lt_typein r).1
              (by
                rw [typein_enum]
                exact lt_succ (typein _ _))).resolve_right
        ab⟩,
    e⟩

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