ofLE_comp_proj — Mathlib

English

The composition of the induced map with A.proj equals B.proj, i.e., ofLE h ∘ A.proj = B.proj.

Русский

Сведение индуцированного отображения к проекции после рефинемента даёт то же, что и проекция B: ofLE(h) ∘ A.proj = B.proj.

LaTeX

$$$$\\mathrm{ofLE}(h) \\circ \\mathrm{A.proj} = \\mathrm{B.proj}.$$$$

Lean4

@[simp]
theorem ofLE_comp_proj (h : A ≤ B) : ofLE h ∘ A.proj = B.proj :=
  funext <| ofLE_proj _

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