ofLE_comp_ofLE — Mathlib

English

Given h1: A ≤ B and h2: B ≤ C, the composed map equals the map corresponding to the transitive refinement A ≤ C.

Русский

Даны h1: A ≤ B и h2: B ≤ C; композиция отображений соответствует отображению для перехода A ≤ C.

LaTeX

$$$$\\forall h_1 : A \\le B,\\; h_2 : B \\le C,\\; (\\,\\mathrm{ofLE}\\, h_2\\circ \\mathrm{ofLE}\\, h_1 = \\mathrm{ofLE}\\, (h_1\\;\\mathrm{trans}\\; h_2)\\,).$$$$

Lean4

@[simp]
theorem ofLE_comp_ofLE (h₁ : A ≤ B) (h₂ : B ≤ C) : ofLE h₂ ∘ ofLE h₁ = ofLE (le_trans h₁ h₂) :=
  funext <| ofLE_ofLE _ _

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