compl_mem_iff

Mathlib.Order.BooleanSubalgebra

URI: https://scilib.ai/kg/mathlib#BooleanSubalgebra.compl_mem_iff

English

a^c ∈ L iff a ∈ L.

Русский

a^c ∈ L эквивалентно a ∈ L.

LaTeX

$$$ a^{\complement} \in L \iff a \in L $$$

Lean4

@[simp]
theorem compl_mem_iff : aᶜ ∈ L ↔ a ∈ L :=
  ⟨fun ha ↦ by simpa using compl_mem ha, compl_mem⟩

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

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

Разделы

Аффилиация

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