disjoint_iSup₂_iff — Mathlib

English

Let a be an element of a frame α and f : ∀ i, κ i → α a two-parameter family. Then a is disjoint from the supremum of all f(i, j) exactly when a is disjoint from each f(i, j).

Русский

Пусть a ∈ α и f : ∀ i, κ i → α задаёт двумерную семейство элементов. Тогда a несовместим с ⨆_{i, j} f(i, j) тогда и только тогда, когда a несовместим с каждым f(i, j).

LaTeX

$$$\operatorname{Disjoint}\left(a, \bigvee_{i} \bigvee_{j} f(i,j)\right) \iff \forall i \forall j\, \operatorname{Disjoint}\left(a, f(i,j)\right)$$$

Lean4

theorem disjoint_iSup₂_iff {f : ∀ i, κ i → α} : Disjoint a (⨆ (i) (j), f i j) ↔ ∀ i j, Disjoint a (f i j) := by
  simp_rw [disjoint_iSup_iff]

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