ofLE_ofLE — Mathlib

English

If h1: A ≤ B and h2: B ≤ C, then the composed refinement yields a refinement A ≤ C, and the corresponding induced maps compose accordingly.

Русский

Если h1: A ≤ B и h2: B ≤ C, то композиция рефинемента даёт A ≤ C, а соответствующие индуцированные отображения композиционны.

LaTeX

$$$$\\forall h_1 : A \\le B,\\; h_2 : B \\le C,\\; x: A,\\; \\mathrm{ofLE}(h_2)(\\mathrm{ofLE}(h_1)(x)) = \\mathrm{ofLE}(h_1\\;{\\buildrel{\\text{trans}}\\over{\\phantom{a}}}\\;h_2)(x).$$$$

Lean4

@[simp]
theorem ofLE_ofLE (h₁ : A ≤ B) (h₂ : B ≤ C) (x : A) : ofLE h₂ (ofLE h₁ x) = ofLE (h₁.trans h₂) x :=
  by
  rcases x with ⟨⟩
  rfl

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