mem_cocardinal

Mathlib.Order.Filter.Cocardinal

URI: https://scilib.ai/kg/mathlib#Filter.mem_cocardinal

English

There is an instance showing that cocardinal α hreg has a CardinalInterFilter with bound c.

Русский

Существуют экземпляры, показывающие, что cocardinal α hreg имеет CardinalInterFilter с границей c.

LaTeX

$$CardinalInterFilter (cocardinal α hreg) c$$

Lean4

@[simp]
theorem mem_cocardinal {s : Set α} : s ∈ cocardinal α hreg ↔ Cardinal.mk (sᶜ : Set α) < c :=
  Iff.rfl

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

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

Разделы

Аффилиация

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