lsub_le_of_range_subset — Mathlib

English

If the range of f is contained in the range of g, then lsub f ≤ lsub g.

Русский

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

LaTeX

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

Lean4

theorem lsub_le_of_range_subset {ι ι'} {f : ι → Ordinal} {g : ι' → Ordinal} (h : Set.range f ⊆ Set.range g) :
    lsub.{u, max v w} f ≤ lsub.{v, max u w} g :=
  csSup_le_csSup' (bddAbove_range.{v, max u w} _) (by convert Set.image_mono h <;> apply Set.range_comp)

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