codisjoint_left

Mathlib.Data.Finset.BooleanAlgebra

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

English

Codisjoint s t is equivalent to ∀ a, a ∉ s → a ∈ t.

Русский

Codisjoint s t эквивалентно ∀ a, a ∉ s → a ∈ t.

LaTeX

$$$\text{Codisjoint}(s,t) \iff \forall a, a \notin s \rightarrow a \in t$$$

Lean4

theorem codisjoint_left : Codisjoint s t ↔ ∀ ⦃a⦄, a ∉ s → a ∈ t := by
  classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]

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

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

Разделы

Аффилиация

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