inf_map_atTop_neBot_iff — Mathlib

English

Let F be a filter on β and u: α→β with [IsDirected α (≤)]. Then NeBot (F ⊓ map u atTop) holds exactly when for every U in F and every N there exists n ≥ N with u(n) ∈ U.

Русский

Пусть F — фильтр на β и u: α→β, α направлен по ≤. Тогда NeBot (F ⊓ map u atTop) эквивалентно тому, что для каждого U ∈ F и для каждого N существует n ≥ N такой, что u(n) ∈ U.

LaTeX

$$$\NeBot(F \sqcap map\ u\ atTop) \iff \forall U \in F, \forall N, \exists n \ge N, u(n) \in U$$$

Lean4

theorem inf_map_atTop_neBot_iff [Nonempty α] : NeBot (F ⊓ map u atTop) ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U := by
  simp_rw [inf_neBot_iff_frequently_left, frequently_map, frequently_atTop]; rfl

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