subtype_coe_map_comap — Mathlib

English

If f is a filter on α and c: β → α, and range c ∈ f while W ∈ comap c f, then c''W ∈ f.

Русский

Если f — фильтр на α и c: β → α с range c ∈ f и W ∈ comap c f, тогда образ c''W ∈ f.

LaTeX

$$$ c '' W \\in f $ given $ W \\in comap\\ c\\ f$ and $range\\ c ∈ f$$$

Lean4

theorem subtype_coe_map_comap (s : Set α) (f : Filter α) : map ((↑) : s → α) (comap ((↑) : s → α) f) = f ⊓ 𝓟 s := by
  rw [map_comap, Subtype.range_coe]

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