Theorems · Theorem · functional analysis

Filter.Eventually.segment_of_prod_nhds

∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {α : Type u_2} {f : Filter α} {x : E}
  {y z : α → E} {r : α → E → Prop},
  Filter.Tendsto y f (nhds x) →
    Filter.Tendsto z f (nhds x) →
      (∀ᶠ (p : α × E) in f ×ˢ nhds x, r p.1 p.2) → ∀ᶠ (χ : α) in f, ∀ v ∈ segment ℝ (y χ) (z χ), r χ v

Defined in

Mathlib.Analysis.Normed.Module.Convex

Cited by

1 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupNormedSpace