English
If a is disjoint from the supremum of a directed family s, then a is disjoint from every member of s; conversely, this implication holds under the given directedness. Formally: Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b.
Русский
Если a параллельно непересекается с верховой гранью направленного семейства s, то a непересекается с каждым элементом этой семейства; обратно тоже верно при заданном направлении. Формально: Disjoint a (sSup s) ⇔ ∀ b ∈ s, Disjoint a b.
LaTeX
$$$ \mathrm{Disjoint}(a, \operatorname{sSup} s) \;\Longleftrightarrow\; \forall b \in s, \mathrm{Disjoint}(a, b) $$$
Lean4
protected theorem disjoint_sSup_right (h : DirectedOn (· ≤ ·) s) : Disjoint a (sSup s) ↔ ∀ ⦃b⦄, b ∈ s → Disjoint a b :=
by simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]
