nonempty_monotone_mem — Mathlib

English

Duplicate of nonempty monotone mem for eVariationOn: if s is nonempty, there exists a monotone u with u i ∈ s for all i.

Русский

Дубликат предыдущего утверждения: если s непусто, существует монотонная последовательность u с u i ∈ s для всех i.

LaTeX

$$eVariationOn.nonempty_monotone_mem {s : Set α} (hs : s.Nonempty) : Nonempty { u // Monotone u ∧ ∀ i : Nat, u i ∈ s }$$

Lean4

theorem nonempty_monotone_mem {s : Set α} (hs : s.Nonempty) : Nonempty { u // Monotone u ∧ ∀ i : ℕ, u i ∈ s } :=
  by
  obtain ⟨x, hx⟩ := hs
  exact ⟨⟨fun _ => x, fun i j _ => le_rfl, fun _ => hx⟩⟩

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