dual_map — Mathlib

English

For every order-preserving map f: α →o β and every NonemptyInterval a ⊆ α, the dual of the image a.map f equals the image of the dual interval under the dual map: dual(a.map f) = a.dual.map f.dual.

Русский

Для каждого порядок-отображения f: α →o β и каждого ненулевого интервала a ⊆ α выполняется: dual(a.map f) = a.dual.map f.dual.

LaTeX

$$$\text{dual}(a.map f) = a.dual.map f.dual$$$

Lean4

@[simp]
theorem dual_map (f : α →o β) (a : NonemptyInterval α) : dual (a.map f) = a.dual.map f.dual :=
  rfl

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