English
For a finite index set consisting of two elements i and j with i ≠ j, the two-point set {i,j} is SupIndep with respect to f if and only if f(i) and f(j) are disjoint.
Русский
Пусть i ≠ j. Тогда множество {i,j} является SupIndep относительно f ⇔ Disjoint(f(i), f(j)).
LaTeX
$$$({ i, j } : Finset ι).SupIndep f \\iff Disjoint (f i) (f j) \\quad (i \\neq j)$$$
Lean4
@[simp]
theorem supIndep_pair [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
({ i, j } : Finset ι).SupIndep f ↔ Disjoint (f i) (f j) :=
by
suffices Disjoint (f i) (f j) → Disjoint (f j) ((Finset.erase { i, j } j).sup f) by
simpa [supIndep_iff_disjoint_erase, hij]
rw [pair_comm]
simp [hij.symm, disjoint_comm]
