map_comp — Mathlib

English

For order-homomorphisms g: β →o γ and f: α →o β, the induced map on upper-set spaces satisfies map(g ∘ f) = (map g) ∘ (map f).

Русский

Для отображений по порядкам g: β →o γ и f: α →o β выполняется равенство, что отображение верхних множеств от композиции g ∘ f эквивалентно композиции соответствующих отображений верхних множеств.

LaTeX

$$$\\mathrm{Topology.WithUpperSet.map}(g \\circ f) = (\\mathrm{Topology.WithUpperSet.map}(g)) \\circ (\\mathrm{Topology.WithUpperSet.map}(f)).$$$

Lean4

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

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