mem_carrier

Mathlib.Order.BooleanSubalgebra

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

English

Let L be a Boolean subalgebra of α. For any a ∈ α, a ∈ L.carrier if and only if a ∈ L.

Русский

Пусть L — булева подпалгебра α. Для любого a ∈ α верно: a ∈ L.carrier тогда и только тогда, когда a ∈ L.

LaTeX

$$$a \in L.\mathrm{carrier} \iff a \in L$$$

Lean4

theorem mem_carrier : a ∈ L.carrier ↔ a ∈ L :=
  .rfl

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

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

Разделы

Аффилиация

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