compl_mem_comk — Mathlib

English

For any property p on sets, and appropriate closure hypotheses, s^c ∈ comk p he hmono hunion if and only if p s.

Русский

Для произвольного свойства p над множествами и подходящих условий замыкания, включение s^c в comk p равносильно p(s).

LaTeX

$$$$ s^{\\complement} \\in comk\ p\ he\ hmono\ hunion \\iff p\\ s $$$$

Lean4

theorem compl_mem_comk {p : Set α → Prop} {he hmono hunion s} : sᶜ ∈ comk p he hmono hunion ↔ p s := by simp

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