le_comap_top — Mathlib

English

Let f: α → β and l be a filter on α. Then l ≤ comap f ⊤; equivalently, comap f ⊤ = ⊤, so every filter on α is below the pullback of the indiscrete filter on β.

Русский

Пусть f: α → β и ℱ — фильтр на α. Тогда ℱ ≤ comap f ⊤; эквивалентно comap f ⊤ = ⊤, то есть любой фильтр на α лежит в нисходящей части pullback индифферентного фильтра на β.

LaTeX

$$$ l \\le \\operatorname{comap}_f(\\top) $$$

Lean4

theorem le_comap_top (f : α → β) (l : Filter α) : l ≤ comap f ⊤ :=
  by
  rw [comap_top]
  exact le_top

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