Commit 2023-07-01 10:00 db4aced9

View on Github →

feat: add Trivialization.tendsto_nhds_iff (#5489) This lemma generalizes FiberBundle.continuousWithinAt_totalSpace. Also add a version with equality of filters.

Estimated changes

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

added theorem Trivialization.nhds_eq_inf_comap

added theorem Trivialization.tendsto_nhds_iff