blsub_le_of_brange_subset — 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

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

Lean4

theorem blsub_le_of_brange_subset {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal} (h : brange o f ⊆ brange o' g) :
    blsub.{u, max v w} o f ≤ blsub.{v, max u w} o' g :=
  bsup_le_of_brange_subset.{u, v, w} fun a ⟨b, hb, hb'⟩ =>
    by
    obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩
    simp_rw [← hc'] at hb'
    exact ⟨c, hc, hb'⟩

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