dual_map — Mathlib

English

The dual of the mapped interval corresponds to mapping the duals: dual (s.map f) = s.dual.map f.dual.

Русский

Дуальная проекция отображения соответствует отображению дуалов: дуал(объект.карта) = дуал(объекта).дуал.

LaTeX

$$$ \mathrm{dual\_map}(f)(s) :\; \text{simp} \Rightarrow \mathrm{dual}(s.map f) = s.dual.map f.dual $$$

Lean4

@[simp]
theorem dual_map (f : α →o β) (s : Interval α) : dual (s.map f) = s.dual.map f.dual :=
  by
  cases s
  · rfl
  · exact WithBot.map_comm rfl _

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