disjoint_coe — Mathlib

English

Disjointness is preserved under passage to sets via conversion between finsets and sets: Disjoint (s.toSet) (t.toSet) iff Disjoint s t.

Русский

Не пересечение сохраняется при переходе между конечными множествами и их множествами: Disjoint (s.toSet) (t.toSet) ⇔ Disjoint s t.

LaTeX

$$$\\operatorname{Disjoint}(s^{toSet}, t^{toSet}) \\iff \\operatorname{Disjoint}(s,t)$$$

Lean4

@[simp, norm_cast]
theorem disjoint_coe : Disjoint (s : Set α) t ↔ Disjoint s t := by
  simp only [Finset.disjoint_left, Set.disjoint_left, mem_coe]

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