inf_map_atBot_neBot_iff — Mathlib

English

A duplicate entry of inf map atTop nonbottom; same content as 158017 but repeated here for completeness.

Русский

Дублирующий пункт для инфимации на atTop; аналогично 158017.

LaTeX

$$$\text{NeBot}(F \cap map\ u\ atTop) \iff \forall U \in F, \forall N, \exists n \ge N, u(n) \in U$$$

Lean4

theorem inf_map_atBot_neBot_iff : NeBot (F ⊓ map u atBot) ↔ ∀ U ∈ F, ∀ N, ∃ n ≤ N, u n ∈ U :=
  inf_map_atTop_neBot_iff (α := αᵒᵈ)

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