iSup₂_eq_bot — Mathlib

English

Let f(i1, i2) be a function of two index variables with values in α. The supremum over all i1,i2 equals ⊥ if and only if every value f(i1,i2) equals ⊥.

Русский

Пусть f(i1,i2) — функция двух переменных индексов. Тогда ⨆_{i1,i2} f(i1,i2) = ⊥ тогда, когда все значения равны ⊥.

LaTeX

$$$$\bigvee_{i_1, i_2} f(i_1,i_2) = \bot \;\Longleftrightarrow\; \forall i_1,i_2,\; f(i_1,i_2) = \bot.$$$$

Lean4

theorem iSup₂_eq_bot {f : ∀ i, κ i → α} : ⨆ (i) (j), f i j = ⊥ ↔ ∀ i j, f i j = ⊥ := by simp

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