mono — Mathlib

English

Monotone inclusion preserves accumulation: if S ⊆ T and o is an accumulation point of S, then o is an accumulation point of T.

Русский

Монотонное включение сохраняет накопления: если S ⊆ T и o — точка накопления S, то o — точка накопления T.

LaTeX

$$mono {o} {S T} (h : S ⊆ T) (ho : o.IsAcc S) : o.IsAcc T$$

Lean4

theorem mono {o : Ordinal} {S T : Set Ordinal} (h : S ⊆ T) (ho : o.IsAcc S) : o.IsAcc T :=
  by
  rw [isAcc_iff] at *
  exact ⟨ho.1, fun p plto ↦ (ho.2 p plto).casesOn fun s hs ↦ ⟨s, h hs.1, hs.2⟩⟩

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