image_coe_mem_of_mem_comap

Mathlib.Order.Filter.Map

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

← MathLib Explorer

English

If f ∈ Filter α and W ∈ comap Subtype.val f, then (Subtype.val) '' W ∈ f.

Русский

Если f ∈ Filter α и W ∈ comap Subtype.val f, то (Subtype.val) '' W ∈ f.

LaTeX

$$$ (\\uparrow) '' W ∈ f $$$

Lean4

theorem image_coe_mem_of_mem_comap {f : Filter α} {U : Set α} (h : U ∈ f) {W : Set U}
    (W_in : W ∈ comap ((↑) : U → α) f) : (↑) '' W ∈ f :=
  image_mem_of_mem_comap (by simp [h]) W_in

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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