disjoint_toFinset — Mathlib

English

Two sets are disjoint iff their Finset enumerations are disjoint.

Русский

Два множества не пересекаются тогда и только тогда, когда их перечисления Finset не пересекаются.

LaTeX

$$$\operatorname{Disjoint}(s.toFinset, t.toFinset) \iff \operatorname{Disjoint}(s,t)$$$

Lean4

@[simp]
theorem disjoint_toFinset [Fintype s] [Fintype t] : Disjoint s.toFinset t.toFinset ↔ Disjoint s t := by
  simp only [← disjoint_coe, coe_toFinset]

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