enumOrd_le_of_subset — Mathlib

English

If s is not bounded above and s ⊆ t, then enumOrd t ≤ enumOrd s.

Русский

Если s не ограничено сверху и s ⊆ t, то enumOrd(t) ≤ enumOrd(s).

LaTeX

$$$$ \\neg BddAbove(s) \\to (s \\subseteq t) \\to \\mathrm{enumOrd}(t) \\le \\mathrm{enumOrd}(s) $$$$

Lean4

theorem enumOrd_le_of_subset {t : Set Ordinal} (hs : ¬BddAbove s) (hst : s ⊆ t) : enumOrd t ≤ enumOrd s :=
  by
  intro a
  rw [enumOrd, enumOrd]
  gcongr with b c
  exacts [enumOrd_nonempty hs a, enumOrd_le_of_subset hs hst c]
termination_by a => a

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