disjoint_left

Mathlib.Data.Set.Disjoint

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

English

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

Русский

Дисjointность s и t эквивалентна ∀ a ∈ s, a ∉ t.

LaTeX

$$$\mathrm{Disjoint}(s,t) \iff \forall a, a \in s \rightarrow a \notin t$$$

Lean4

theorem disjoint_left : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t :=
  disjoint_iff_inf_le.trans <| forall_congr' fun _ => not_and

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

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

Разделы

Аффилиация

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