isBoundedUnder_const — Mathlib

English

If r is reflexive, then for any filter l on β and any a in α, the constant function mapping every element to a is bounded under r along l.

Русский

Пусть r рефлексивна. Тогда для любого фильтра l на β и любого a ∈ α константная функция, возвращающая a, ограничена по r вдоль l.

LaTeX

$$$ [IsRefl\ α\ r] \Rightarrow \forall l : Filter\, β,\ a : α, IsBoundedUnder r l (\text{const}_{a}) $$$

Lean4

theorem isBoundedUnder_const [IsRefl α r] {l : Filter β} {a : α} : IsBoundedUnder r l fun _ => a :=
  ⟨a, eventually_map.2 <| Eventually.of_forall fun _ => refl _⟩

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