disjoint_toFinset — Mathlib

English

Disjointness is preserved when passing to Finset representations: Disjoint hs.toFinset ht.toFinset iff Disjoint s t.

Русский

Дисjointность сохраняется при переходе к представлениям Finset: Disjoint hs.toFinset ht.toFinset ⇔ Disjoint s t.

LaTeX

$$$ \operatorname{Disjoint}(hs.toFinset, ht.toFinset) \Longleftrightarrow \operatorname{Disjoint}(s, t) $$$

Lean4

@[simp]
nonrec theorem disjoint_toFinset {hs : s.Finite} {ht : t.Finite} : Disjoint hs.toFinset ht.toFinset ↔ Disjoint s t :=
  @disjoint_toFinset _ _ _ hs.fintype ht.fintype

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