disjoint_right

Mathlib.Data.Finset.Disjoint

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

English

Disjoint s t is equivalent to ∀ a ∈ t, a ∉ s.

Русский

Непересечение множеств эквивалентно ∀ a ∈ t, a ∉ s.

LaTeX

$$$ \\operatorname{Disjoint}(s,t) \\Leftrightarrow \\forall a\\,(a \\in t \\rightarrow a \\notin s) $$$

Lean4

theorem disjoint_right : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s := by rw [_root_.disjoint_comm, disjoint_left]

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

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

Разделы

Аффилиация

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