bsup_le_of_brange_subset — Mathlib

English

If brange(o,f) is contained in brange(o',g), then o.bsup f ≤ o'.bsup g.

Русский

Если brange(o,f) ⊆ brange(o',g), то o.bsup f ≤ o'.bsup g.

LaTeX

$$$brange(o,f) \\subseteq brange(o',g) \\Rightarrow o.bsup f \\le o'.bsup g$$$

Lean4

theorem bsup_le_of_brange_subset {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal} (h : brange o f ⊆ brange o' g) :
    bsup.{u, max v w} o f ≤ bsup.{v, max u w} o' g :=
  bsup_le fun i hi => by
    obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, rfl⟩
    rw [← hj']
    apply le_bsup

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