ord_cof_eq — Mathlib

English

There exists an unbounded S such that type(Subrel r (· ∈ S)) equals cof(type r).ord.

Русский

Существует неограниченное S такое, что type(Subrel r)^{ord} = cof(type r)^{ord}.

LaTeX

$$$\\exists S, Unbounded\\ r S \\land type(Subrel\\ r\\ (\\cdot \\in S)).ord = cof(type\\; r).ord$$$

Lean4

theorem ord_cof_eq (r : α → α → Prop) [IsWellOrder α r] :
    ∃ S, Unbounded r S ∧ type (Subrel r (· ∈ S)) = (cof (type r)).ord :=
  by
  let ⟨S, hS, e⟩ := cof_eq r
  let ⟨s, _, e'⟩ := Cardinal.ord_eq S
  let T : Set α := {a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a}
  suffices Unbounded r T
    by
    refine ⟨T, this, le_antisymm ?_ (Cardinal.ord_le.2 <| cof_type_le this)⟩
    rw [← e, e']
    refine
      (RelEmbedding.ofMonotone
          (fun a : T =>
            (⟨a,
                let ⟨aS, _⟩ := a.2
                aS⟩ :
              S))
          fun a b h => ?_).ordinal_type_le
    rcases a with ⟨a, aS, ha⟩
    rcases b with ⟨b, bS, hb⟩
    change s ⟨a, _⟩ ⟨b, _⟩
    refine ((trichotomous_of s _ _).resolve_left fun hn => ?_).resolve_left ?_
    · exact asymm h (ha _ hn)
    · intro e
      injection e with e
      subst b
      exact irrefl _ h
  intro a
  have : {b : S | ¬r b a}.Nonempty :=
    let ⟨b, bS, ba⟩ := hS a
    ⟨⟨b, bS⟩, ba⟩
  let b := (IsWellFounded.wf : WellFounded s).min _ this
  have ba : ¬r b a := IsWellFounded.wf.min_mem _ this
  refine ⟨b, ⟨b.2, fun c => not_imp_not.1 fun h => ?_⟩, ba⟩
  rw [show ∀ b : S, (⟨b, b.2⟩ : S) = b by intro b; cases b; rfl]
  exact IsWellFounded.wf.not_lt_min _ this (IsOrderConnected.neg_trans h ba)

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