smaller_factorization — Mathlib

English

Compatibility of smaller with πs map holds: a simple equality of compositions.

Русский

Совместимость меньшего с отображением πs: простое равенство композиции.

LaTeX

$$$$ (\\mathrm{fun} p \\mapsto p.1) \\circ (\\mathrm{range\\_equiv\\_smaller}\\; C\\; o) = (\\mathrm{πs}\\; C\\; o) \\circ (\\mathrm{fun} p \\mapsto p.1) $$$$

Lean4

theorem smaller_factorization (o : Ordinal) :
    (fun (p : smaller C o) ↦ p.1) ∘ (range_equiv_smaller C o).toFun =
      (πs C o) ∘ (fun (p : range (π C (ord I · < o))) ↦ p.1) :=
  by rfl

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