smaller_mono — Mathlib

English

If o1 ≤ o2 then smaller C o1 ⊆ smaller C o2.

Русский

Если o1 ≤ o2, то smaller C o1 вложено в smaller C o2.

LaTeX

$$$$ o_1 \\le o_2 \\;\\Rightarrow\\; smaller\\; C\\; o_1 \\subseteq smaller\\; C\\; o_2 $$$$

Lean4

theorem smaller_mono {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) : smaller C o₁ ⊆ smaller C o₂ :=
  by
  rintro f ⟨g, hg, rfl⟩
  simp only [smaller, Set.mem_image]
  use πs' C h g
  obtain ⟨⟨l, gl⟩, rfl⟩ := hg
  refine ⟨?_, ?_⟩
  · use ⟨l, Products.isGood_mono C h gl⟩
    ext x
    rw [eval, ← Products.eval_πs' _ h (Products.prop_of_isGood C _ gl), eval]
  · rw [← LocallyConstant.coe_inj, coe_πs C o₂, ← LocallyConstant.toFun_eq_coe, coe_πs', Function.comp_assoc,
      projRestricts_comp_projRestrict C _, coe_πs]
    rfl

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