map_ofDual_max — Mathlib

English

In the dual order, the maximum corresponds to the minimum; mapping by the dual interchanges max and min.

Русский

В порядке двойственном максимум соответствует минимуму; отображение через дуальное отображение меняет max на min.

LaTeX

$$$\\text{For a finite } S \\subseteq \\alpha^{\\mathrm{op}},\\; \\mathrm{map\\_ofDual\\_max}(S) = \\mathrm{min}'(\\mathrm{image}(\\mathrm{ofDual}, S)).$$$

Lean4

theorem map_ofDual_max (s : Finset αᵒᵈ) : s.max.map ofDual = (s.image ofDual).min :=
  by
  rw [min_eq_inf_withTop, inf_image]
  exact congr_fun WithTop.map_id _

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