mk_comp_mk — Mathlib

English

Let f: α →o β and g: β →o γ be monotone maps between preorders. Then the composition of their bundled monotone maps is the bundled monotone map with underlying function g ∘ f and monotonicity given by hg ∘ hf.

Русский

Пусть f: α →o β и g: β →o γ — монотонные отображения между предпорядками. Тогда композиция их упакованных монотонных отображений есть упакованное монотонное отображение с функцией g ∘ f и монотонностью hg ∘ hf.

LaTeX

$$$ (g,h_g) \circ (f,h_f) = (g\circ f, h_g \circ h_f) $$$

Lean4

@[simp]
theorem mk_comp_mk (g : β → γ) (f : α → β) (hg hf) : comp ⟨g, hg⟩ ⟨f, hf⟩ = ⟨g ∘ f, hg.comp hf⟩ :=
  rfl

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