lsub_eq_of_range_eq — Mathlib

English

If Set.range f = Set.range g, then lsub f = lsub g.

Русский

Если образ f равен образу g, то lsub f = lsub g.

LaTeX

$$$\operatorname{range}(f) = \operatorname{range}(g) \Rightarrow \operatorname{lsub} f = \operatorname{lsub} g$$$

Lean4

theorem lsub_eq_of_range_eq {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal} (h : Set.range f = Set.range g) :
    lsub.{u, max v w} f = lsub.{v, max u w} g :=
  (lsub_le_of_range_subset.{u, v, w} h.le).antisymm (lsub_le_of_range_subset.{v, u, w} h.ge)

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