image_mem_of_mem_comap

Mathlib.Order.Filter.Map

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

← MathLib Explorer

English

If U ∈ f and W ∈ comap c f with W ⊆ U, then c(W) ∈ f.

Русский

Если U ∈ f и W ∈ comap c f с W ⊆ U, то c(W) ∈ f.

LaTeX

$$$ W \\in comap c f \\; \\Rightarrow \\; c''W \\in f $$$

Lean4

theorem image_mem_of_mem_comap {f : Filter α} {c : β → α} (h : range c ∈ f) {W : Set β} (W_in : W ∈ comap c f) :
    c '' W ∈ f := by
  rw [← map_comap_of_mem h]
  exact image_mem_map W_in

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

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

Разделы

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

Аффилиация

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