map_toDual_min — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_toDual_min (s : Finset α) : s.min.map toDual = (s.image toDual).max :=
  by
  rw [max_eq_sup_withBot, sup_image]
  exact congr_fun WithBot.map_id _

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