map_toDual_max — Mathlib

English

The maximum of a finite set, when mapped by toDual, equals the minimum of its image under toDual.

Русский

Максимум множества, образованный через toDual, равен минимуму образов через toDual.

LaTeX

$$$\\operatorname{toDual}(\\max' S) = \\min'(\\operatorname{image}(\\operatorname{toDual}, S)).$$$

Lean4

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

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