bsup_eq_of_brange_eq — Mathlib

English

If brange o f equals brange o' g, then bsup o f equals bsup o' g.

Русский

Если brange o f = brange o' g, то bsup o f = bsup o' g.

LaTeX

$$$brange(o,f) = brange(o',g) \\Rightarrow bsup(o,f) = bsup(o',g)$$$

Lean4

theorem bsup_eq_of_brange_eq {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_of_brange_subset.{u, v, w} h.le).antisymm (bsup_le_of_brange_subset.{v, u, w} h.ge)

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