compl_mem_comap

Mathlib.Order.Filter.Map

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

English

The complement version: sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l.

Русский

Версия для дополнения: s^c ∈ comap f l ⇔ (f '' s)^c ∈ l.

LaTeX

$$sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l$$

Lean4

theorem compl_mem_comap : sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l := by rw [mem_comap_iff_compl, compl_compl]

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

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

Разделы

Аффилиация

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