English
Let a,b be elements and c,d sets with hs,ht providing pointwise bounds e ≤ a for e ∈ c and e ≤ b for e ∈ d, and hd: Disjoint a b, he: ⊥ ∉ c ∨ ⊥ ∉ d. Then Disjoint c d.
Русский
Пусть a,b — элементы, c,d — множества; предположения hs, ht задают покрёпленные границы e ≤ a для e∈c и e ≤ b для e∈d, hd: несоотносимость a и b, и e: ⊥ не в c или в d. Тогда Disjoint c d.
LaTeX
$$$\forall a,b,c,d\, (hs: \forall e \in c, e \le a) (ht: \forall e \in d, e \le b) (hd: Disjoint a b) (he: ⊥ \notin c \lor ⊥ \notin d),\; Disjoint c d$$$
Lean4
theorem disjoint_of_sSup_disjoint_of_le_of_le {a b : α} {c d : Set α} (hs : ∀ e ∈ c, e ≤ a) (ht : ∀ e ∈ d, e ≤ b)
(hd : Disjoint a b) (he : ⊥ ∉ c ∨ ⊥ ∉ d) : Disjoint c d :=
by
rw [disjoint_iff_forall_ne]
intro x hx y hy
rw [Disjoint.ne_iff]
· aesop
· exact Disjoint.mono (hs x hx) (ht y hy) hd
