blsub_eq_of_brange_eq — Mathlib

English

If brange o f ⊆ brange o' g then blsub o f ≤ blsub o' g.

Русский

Если brange o f ⊆ brange o' g, тогда blsub o f ≤ blsub o' g.

LaTeX

$$$ \\text{brange}(o,f) \\subseteq \\text{brange}(o',g) \\Rightarrow \\operatorname{blsub}(o,f) \\le \\operatorname{blsub}(o',g) $$$

Lean4

theorem blsub_eq_of_brange_eq {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal}
    (h : {o | ∃ i hi, f i hi = o} = {o | ∃ i hi, g i hi = o}) : blsub.{u, max v w} o f = blsub.{v, max u w} o' g :=
  (blsub_le_of_brange_subset.{u, v, w} h.le).antisymm (blsub_le_of_brange_subset.{v, u, w} h.ge)

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