disjoint_val

Mathlib.Data.Finset.Disjoint

URI: https://scilib.ai/kg/mathlib#Finset.disjoint_val

English

If h is a Disjoint s t, then for any a ∈ s and b ∈ t, a ≠ b.

Русский

Если h : Disjoint s t, то для любого a ∈ s и b ∈ t, a ≠ b.

LaTeX

$$$ \\forall h:\\operatorname{Disjoint}(s,t), \\forall a\\in s, \\forall b\\in t, a \\neq b$$$

Lean4

@[simp]
theorem disjoint_val : Disjoint s.1 t.1 ↔ Disjoint s t :=
  Multiset.disjoint_left.trans disjoint_left.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru