map_ciInf — Mathlib

English

Let e be an order isomorphism; the infimum over a family f:ι→α is preserved: e(⨅ i, f(i)) = ⨅ i, e(f(i)).

Русский

Пусть e — отображение упорядочивающего типа; инфимуум сохраняется: e(⨅i f(i)) = ⨅i e(f(i)).

LaTeX

$$$e\\Big(\\bigwedge_{i} f(i)\\Big) = \\bigwedge_{i} e\\big(f(i)\\big)$$$

Lean4

theorem map_ciInf (e : α ≃o β) {f : ι → α} (hf : BddBelow (range f)) : e (⨅ i, f i) = ⨅ i, e (f i) :=
  e.dual.map_ciSup hf

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