toDualProd_apply — Mathlib

English

For any nonempty interval s in α, the canonical map to the dual-ordered product yields s.toDualProd = (toDual s.fst, s.snd).

Русский

Пусть s — непустой интервал в α. Тогда каноническое отображение в произведение αᵒᵈ × α задаёт: s.toDualProd = (toDual s.fst, s.snd).

LaTeX

$$$s.toDualProd = (toDual\, s.fst, s.snd)$$$

Lean4

@[simp]
theorem toDualProd_apply (s : NonemptyInterval α) : s.toDualProd = (toDual s.fst, s.snd) :=
  rfl

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