map_csInf — Mathlib

English

For e an order isomorphism and any set s, the image under e of the infimum over s equals the infimum of the images, provided the set is nonempty and bounded below.

Русский

Пусть e — отображение, сохраняющее порядок, и есть непустое множество s; если s ограничено снизу, то e( sInf s ) = ⨅ x∈s, e(x).

LaTeX

$$$e\\left(s\\inf s\\right) = \\inf_{x\\in s} e(x)$$$

Lean4

theorem map_csInf (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : e (sInf s) = ⨅ x : s, e x :=
  e.dual.map_csSup hne hbdd

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