map_map — Mathlib

English

Let α, β, γ be preordered sets. For any nonempty interval a ∈ NonemptyInterval α and order-preserving maps f: α →o β, g: β →o γ, one has (a.map f).map g = a.map (g ∘ f).

Русский

Пусть α, β, γ упорядоченные множества. Пусть a ∈ NonemptyInterval α — ненулевой интервал, и существуют порядок-отображения f: α →o β, g: β →o γ. Тогда (a.map f).map g = a.map (g ∘ f).

LaTeX

$$$ (a.map f).map g = a.map (g \circ f) $$$

Lean4

@[simp]
theorem map_map (g : β →o γ) (f : α →o β) (a : NonemptyInterval α) : (a.map f).map g = a.map (g.comp f) :=
  rfl

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