sdiff_mem

Mathlib.Order.BooleanSubalgebra

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

English

If a,b ∈ L, then a \ b ∈ L.

Русский

Если a,b ∈ L, то a \ b ∈ L.

LaTeX

$$$ a \in L \rightarrow b \in L \rightarrow a \\ b \in L $$$

Lean4

theorem sdiff_mem (ha : a ∈ L) (hb : b ∈ L) : a \ b ∈ L := by simpa [sdiff_eq] using L.infClosed ha (compl_mem hb)

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

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

Разделы

Аффилиация

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