Theorems · Definition · general topology

Filter.comap

{α : Type u_1} → {β : Type u_2} → (α → β) → Filter β → Filter α

The inverse map of a filter. A set s belongs to Filter.comap m f if either of the following equivalent conditions hold. 1. There exists a set t ∈ f such that m ⁻¹' t ⊆ s. This is used as a definition. 2. The set kernImage m s = {y | ∀ x, m x = y → x ∈ s} belongs to f, see Filter.mem_comap'. 3. The set (m '' sᶜ)ᶜ belongs to f, see Filter.mem_comap_iff_compl and Filter.compl_mem_comap.

Defined in

Mathlib.Order.Filter.Defs

Cited by

546 results in Mathlib

Foundations

Depth 58 from the axioms, rests on 652 definitions · uses propext, Classical.choice, Quot.sound