map_iInf — Mathlib

English

Let f be an order isomorphism between complete lattices α and β. Then for any x: ι → α, f(⨅ i, x(i)) = ⨅ i, f(x(i)).

Русский

Пусть f — порядок-изоморфизм между полными решетками α и β. Тогда для любого x: ι → α выполняется f(∧_i x(i)) = ∧_i f(x(i)).

LaTeX

$$$f\\\\left(\\\\big\\\\wedge_{i} x_i\\\\right) = \\\\big\\\\wedge_{i} f(x_i)$$$

Lean4

theorem map_iInf [CompleteLattice β] (f : α ≃o β) (x : ι → α) : f (⨅ i, x i) = ⨅ i, f (x i) :=
  OrderIso.map_iSup f.dual _

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