English
For fixed distinct i ≠ j and every k, k ∈ {i, j}, iSupIndep t is equivalent to Disjoint (t i) (t j).
Русский
Для фиксированных различных i ≠ j и каждого k, где k ∈ {i, j}, iSupIndep t эквивалентно тому, что t i и t j — независимы (дисjoint).
LaTeX
$$$\\\\forall i \\\\neq j,\\\\ \\,\\\\forall k, (k=i \\\\lor k=j) \\\\Rightarrow iSupIndep(t) \\\\iff Disjoint(t(i), t(j))$$$
Lean4
theorem iSupIndep_pair {i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j) : iSupIndep t ↔ Disjoint (t i) (t j) :=
by
constructor
· exact fun h => h.pairwiseDisjoint hij
· rintro h k
obtain rfl | rfl := huniv k
· refine h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)
rw [(huniv i).resolve_left hi]
· refine h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)
rw [(huniv j).resolve_right hj]
