Skip to content

Commit

Permalink
doc(order/filter/basic): fix notations in doc of filter.comap (#16530)
Browse files Browse the repository at this point in the history
The notations in the doc of ```filter.comap``` did not match the notations used in the lemma and thus were a bit confusing (at least for me).
  • Loading branch information
xroblot committed Sep 17, 2022
1 parent a4f6c41 commit 0ff46b9
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/order/filter/basic.lean
Expand Up @@ -1546,12 +1546,12 @@ end map

section comap

/-- The inverse map of a filter. A set `s` belongs to `filter.comap f l` if either of the following
/-- 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 ∈ l` such that `f ⁻¹' t ⊆ s`. This is used as a definition.
2. The set `{y | ∀ x, f x = y → x ∈ s}` belongs to `l`, see `filter.mem_comap'`.
3. The set `(f '' sᶜ)ᶜ` belongs to `l`, see `filter.mem_comap_iff_compl` and
1. There exists a set `t ∈ f` such that `m ⁻¹' t ⊆ s`. This is used as a definition.
2. The set `{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`. -/
def comap (m : α → β) (f : filter β) : filter α :=
{ sets := { s | ∃ t ∈ f, m ⁻¹' t ⊆ s },
Expand Down

0 comments on commit 0ff46b9

Please sign in to comment.