iSup₂_disjoint_iff — Mathlib

English

For a two-parameter family f, Disjoint (⨆ i f i) a is equivalent to Disjoint (f i j) a for all i, j.

Русский

Для двухпараметрической семейства f: несовместность с ⨆ i f i эквивалентна несовместности с каждым f(i,j).

LaTeX

$$$\\operatorname{Disjoint}\\bigl( \\bigvee_i \\bigvee_j f(i,j), a \\bigr) \\Leftrightarrow \\forall i,\\forall j, \\operatorname{Disjoint}(f(i,j), a)$$$

Lean4

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

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