exists_ordinal — Mathlib

English

For any C, the set of generating monomorphisms is contained in monomorphisms of C.

Русский

Для любого C множество порождающих монообразований содержится в монообразованиях C.

LaTeX

$$$generatingMonomorphisms G \leq \text{monomorphisms } C$$$

Lean4

theorem exists_ordinal (A₀ : Subobject X) :
    ∃ (o : Ordinal.{w}) (j : o.toType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤ :=
  by
  let κ := Order.succ (Cardinal.mk (Shrink.{w} (Subobject X)))
  have : OrderBot κ.ord.toType :=
    Ordinal.toTypeOrderBot
      (by
        simp only [ne_eq, Cardinal.ord_eq_zero]
        apply Cardinal.succ_ne_zero)
  exact ⟨κ.ord, top_mem_range hG A₀ (lt_of_lt_of_le (Order.lt_succ _) (by simp [κ]))⟩

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