disjoint_iff_forall_ne

Mathlib.Data.Set.Disjoint

URI: https://scilib.ai/kg/mathlib#Set.disjoint_iff_forall_ne

← MathLib Explorer

English

Disjoint s t iff ∀ a ∈ s, ∀ b ∈ t, a ≠ b.

Русский

Дисjointность равна ∀ a ∈ s, ∀ b ∈ t, a ≠ b.

LaTeX

$$$\mathrm{Disjoint}(s,t) \iff \forall a \in s, \forall b \in t, a \neq b$$$

Lean4

theorem disjoint_iff_forall_ne : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ t → a ≠ b := by
  simp only [Ne, disjoint_left, @imp_not_comm _ (_ = _), forall_eq']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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