mem_sets

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#FilterBasis.mem_sets

English

For any s and B, s ∈ B.sets if and only if s ∈ B.

Русский

Для любого множества s и базиса B верно, что s ∈ B.sets тогда и только тогда, когда s ∈ B.

LaTeX

$$$s \in B.\text{sets} \leftrightarrow s \in B$$$

Lean4

@[simp]
theorem mem_sets {s : Set α} {B : FilterBasis α} : s ∈ B.sets ↔ s ∈ B :=
  Iff.rfl

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

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

Разделы

Аффилиация

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