disjoint_coe — Mathlib

English

For s, t in LowerSet α, the disjointness of their underlying sets equals the disjointness of s and t as lower sets.

Русский

Для s, t из LowerSet α несоприкосновение их соответствующих множеств совпадает со свойством несоприкосновенности самих s и t как элементов LowerSet.

LaTeX

$$$\text{Disjoint}((s:\mathrm{Set}\alpha), t) \iff \text{Disjoint}(s, t)$$$

Lean4

@[simp, norm_cast]
theorem disjoint_coe : Disjoint (s : Set α) t ↔ Disjoint s t := by simp [disjoint_iff, SetLike.ext'_iff]

Похожие утверждения