Continuity

📁 Source: Mathlib/Topology/OpenPartialHomeomorph/Continuity.lean

Statistics

Metric	Count
Definitions	0
Theorems continuousAt, continuousAt_iff_continuousAt_comp_left, continuousAt_iff_continuousAt_comp_right, continuousAt_symm, continuousOn_iff_continuousOn_comp_left, continuousOn_iff_continuousOn_comp_right, continuousWithinAt_iff_continuousWithinAt_comp_left, continuousWithinAt_iff_continuousWithinAt_comp_right, continuous_iff_continuous_comp_left, eventually_left_inverse, eventually_left_inverse', eventually_ne_nhdsWithin, eventually_nhds, eventually_nhds', eventually_nhdsWithin, eventually_nhdsWithin', eventually_right_inverse, eventually_right_inverse', image_mem_nhds, map_nhdsWithin_eq, map_nhdsWithin_preimage_eq, map_nhds_eq, nhdsWithin_source_inter, nhdsWithin_target_inter, preimage_eventuallyEq_target_inter_preimage_inter, symm_map_nhds_eq, tendsto_symm	27
Total	27

OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	ContinuousAt toFun'	—	ContinuousWithinAt.continuousAt continuousOn IsOpen.mem_nhds open_source
continuousAt_iff_continuousAt_comp_left 📖	mathematical	Set Filter Filter.instMembership nhds Set.preimage PartialEquiv.source toPartialEquiv	ContinuousAt toFun'	—	mem_of_mem_nhds nhdsWithin_univ continuousWithinAt_univ continuousWithinAt_iff_continuousWithinAt_comp_left
continuousAt_iff_continuousAt_comp_right 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	ContinuousAt toFun' symm	—	continuousWithinAt_univ continuousWithinAt_iff_continuousWithinAt_comp_right Set.preimage_univ
continuousAt_symm 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	ContinuousAt toFun' symm	—	continuousAt
continuousOn_iff_continuousOn_comp_left 📖	mathematical	Set Set.instHasSubset Set.preimage PartialEquiv.source toPartialEquiv	ContinuousOn toFun'	—	continuousWithinAt_iff_continuousWithinAt_comp_left Filter.mem_of_superset self_mem_nhdsWithin
continuousOn_iff_continuousOn_comp_right 📖	mathematical	Set Set.instHasSubset PartialEquiv.target toPartialEquiv	ContinuousOn toFun' Set.instInter PartialEquiv.source Set.preimage	—	symm_image_eq_source_inter_preimage continuousWithinAt_iff_continuousWithinAt_comp_right Set.inter_comm continuousWithinAt_inter IsOpen.mem_nhds open_source map_target
continuousWithinAt_iff_continuousWithinAt_comp_left 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv Filter Filter.instMembership nhdsWithin Set.preimage	ContinuousWithinAt toFun'	—	ContinuousAt.comp_continuousWithinAt continuousAt continuousWithinAt_inter' ContinuousWithinAt.comp ContinuousAt.continuousWithinAt continuousAt_symm map_source Set.subset_univ ContinuousWithinAt.congr left_inv
continuousWithinAt_iff_continuousWithinAt_comp_right 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	ContinuousWithinAt toFun' Set.preimage symm	—	Filter.tendsto_map'_iff map_nhdsWithin_preimage_eq map_target right_inv
continuous_iff_continuous_comp_left 📖	mathematical	Set.preimage PartialEquiv.source toPartialEquiv Set.univ	Continuous toFun'	—	continuousOn_iff_continuousOn_comp_left Eq.subset Set.instReflSubset
eventually_left_inverse 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Eventually toFun' symm nhds	—	Filter.Eventually.mono IsOpen.eventually_mem open_source PartialEquiv.left_inv'
eventually_left_inverse' 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	Filter.Eventually toFun' symm nhds	—	eventually_left_inverse map_target
eventually_ne_nhdsWithin 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Eventually toFun' nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet	—	eventually_nhdsWithin_iff Filter.Eventually.mono eventually_left_inverse Set.mem_singleton_iff left_inv
eventually_nhds 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Eventually nhds toFun'	—	map_nhds_eq Filter.eventually_map
eventually_nhds' 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Eventually toFun' symm nhds	—	eventually_nhds Filter.eventually_congr Filter.Eventually.mono eventually_left_inverse
eventually_nhdsWithin 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Eventually nhdsWithin toFun' Set.preimage symm	—	map_nhdsWithin_eq image_source_inter_eq' nhdsWithin_target_inter mapsTo Filter.eventually_map
eventually_nhdsWithin' 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Eventually toFun' symm nhdsWithin Set.preimage	—	eventually_nhdsWithin Filter.eventually_congr Filter.Eventually.mono eventually_nhdsWithin_of_eventually_nhds eventually_left_inverse
eventually_right_inverse 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	Filter.Eventually toFun' symm nhds	—	Filter.Eventually.mono IsOpen.eventually_mem open_target PartialEquiv.right_inv'
eventually_right_inverse' 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Eventually toFun' symm nhds	—	eventually_right_inverse map_source
image_mem_nhds 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv Filter Filter.instMembership nhds	toFun' Set.image	—	Filter.image_mem_map map_nhds_eq
map_nhdsWithin_eq 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.map toFun' nhdsWithin Set.image Set.instInter	—	nhdsWithin_source_inter Set.LeftInvOn.map_nhdsWithin_eq Set.LeftInvOn.mono leftInvOn Set.inter_subset_left left_inv ContinuousAt.continuousWithinAt continuousAt_symm map_source continuousAt
map_nhdsWithin_preimage_eq 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.map toFun' nhdsWithin Set.preimage	—	map_nhdsWithin_eq image_source_inter_eq' target_inter_inv_preimage_preimage nhdsWithin_target_inter map_source
map_nhds_eq 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.map toFun' nhds	—	le_antisymm continuousAt Filter.le_map_of_right_inverse eventually_right_inverse' tendsto_symm
nhdsWithin_source_inter 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	nhdsWithin Set.instInter	—	nhdsWithin_inter_of_mem mem_nhdsWithin_of_mem_nhds IsOpen.mem_nhds open_source
nhdsWithin_target_inter 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	nhdsWithin Set.instInter	—	nhdsWithin_source_inter
preimage_eventuallyEq_target_inter_preimage_inter 📖	mathematical	ContinuousWithinAt Set Set.instMembership PartialEquiv.source toPartialEquiv Filter Filter.instMembership nhds	Filter.EventuallyEq toFun' Set.preimage symm Set.instInter PartialEquiv.target	—	Filter.eventuallyEq_set eventually_nhds Filter.mp_mem mem_nhdsWithin_iff_eventually ContinuousWithinAt.preimage_mem_nhdsWithin IsOpen.mem_nhds open_source Filter.univ_mem' mapsTo left_inv
symm_map_nhds_eq 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.map toFun' symm nhds	—	map_nhds_eq map_source left_inv
tendsto_symm 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Filter.Tendsto toFun' symm nhds	—	left_inv continuousAt_symm map_source

---

← Back to Index