English
If t is independent, then any single t_x is disjoint from the iSup of any subset of the rest.
Русский
Если t независима, то любой t_x дисjoint с iSup множества остальных элементов.
LaTeX
$$$iSupIndep t \\\\Rightarrow \\\\forall x \\\\forall y, x \\\\notin y \\\\Rightarrow Disjoint (t x) (\\\\bigvee_{i \\\\in y} t i)$$$
Lean4
/-- If the elements of a set are independent, then any element is disjoint from the `iSup` of some
subset of the rest. -/
theorem disjoint_biSup {ι : Type*} {α : Type*} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) {x : ι} {y : Set ι}
(hx : x ∉ y) : Disjoint (t x) (⨆ i ∈ y, t i) :=
Disjoint.mono_right (biSup_mono fun _ hi => (ne_of_mem_of_not_mem hi hx :)) (ht x)
