mem_comk

Mathlib.Order.Filter.Defs

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

English

Membership in comk is equivalent to membership of the complement: s ∈ comk p he hmono hunion iff p s^c.

Русский

Членство в comk p … эквивалентно членству комплемента: s ∈ comk p h... iff p(s^c).

LaTeX

$$$\forall {p} {he} {hmono} {hunion} {s}, s \in comk p he hmono hunion \iff p\ s^c$$$

Lean4

@[simp]
theorem mem_comk {p : Set α → Prop} {he hmono hunion s} : s ∈ comk p he hmono hunion ↔ p sᶜ :=
  .rfl

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

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

Разделы

Аффилиация

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