map_iInf₂ — Mathlib

English

Let f be an order isomorphism between α and β. Then for a double-indexed family x(i, j), f(⨅ i, ⨅ j, x(i,j)) = ⨅ i, ⨅ j, f(x(i,j)).

Русский

Пусть f — изоморфизм порядков между α и β. Тогда для двумерной семейной функции x(i,j) выполняется f(∧_i ∧_j x(i,j)) = ∧_i ∧_j f(x(i,j)).

LaTeX

$$$f\\\\left(\\\\big\\\\wedge_{i}\\\\big\\\\wedge_{j} x(i,j)\\\\right) = \\\\big\\\\wedge_{i}\\\\big\\\\wedge_{j} f(x(i,j))$$$

Lean4

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

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