map_csInf' — Mathlib

English

Similar to map_csInf, but with the dual image: e(sInf s) = sInf (e''s) for a nonempty s and bounded below set.

Русский

Аналогично map_csInf; существует равенство e(sInf s) = sInf (e''s) при не пустом s и нижней ограниченности.

LaTeX

$$$e\\left(sInf\\, s\\right) = sInf\\left(e''s\\right)$$$

Lean4

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

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