Theorems · Theorem · general topology

Filter.Eventually.prod_inl_nhds

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {x : X},
  (∀ᶠ (x : X) in nhds x, p x) → ∀ (y : Y), ∀ᶠ (x : X × Y) in nhds (x, y), p x.1

Defined in

Mathlib.Topology.Constructions.SumProd

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace