iInf₂_eq_top — Mathlib

English

Let f(i1,i2) be a two-parameter family with values in α. The infimum over all i1,i2 equals ⊤ if and only if every value f(i1,i2) equals ⊤.

Русский

Пусть f(i1,i2) — двумерная семейство значений в α. Инфимум по всем i1,i2 равен ⊤ тогда и только тогда, когда все значения равны ⊤.

LaTeX

$$$$\bigwedge_{i_1,i_2} f(i_1,i_2) = \top \;\Longleftrightarrow\; \forall i_1,i_2,\; f(i_1,i_2) = \top.$$$$

Lean4

theorem iInf₂_eq_top {f : ∀ i, κ i → α} : ⨅ (i) (j), f i j = ⊤ ↔ ∀ i j, f i j = ⊤ := by simp

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