ContinuousOn

📁 Source: Mathlib/Topology/ContinuousOn.lean

Statistics

Metric	Count
Definitions ContinuousOn	1
Theorems comp_continuousOn, comp_continuousOn', continuousOn, continuousWithinAt, preimage_mem_nhdsSet, preimage_mem_nhdsSetWithin, tendsto_nhdsSet, tendsto_nhdsSet_nhds, comp_continuousWithinAt, comp_continuousWithinAt_of_eq, comp₂_continuousWithinAt, comp₂_continuousWithinAt_of_eq, congr_of_eventuallyEq, continuousWithinAt, comp, comp', comp_continuous, comp_inter, congr_mono, continuousAt, continuousWithinAt, finCons, finInsertNth, finSnoc, fst, iUnion_of_isOpen, image_closure, image_comp_continuous, isOpen_inter_preimage, isOpen_preimage, iterate, mapsToRestrict, matrixVecCons, mono, mono_dom, mono_rng, preimage_interior_subset_interior_preimage, preimage_isClosed_of_isClosed, preimage_mem_nhdsSetWithin, preimage_mem_nhdsSetWithin_of_mem_nhdsSet, prodMap, prodMk, restrict, snd, tendsto_nhdsSet, uncurry_left, uncurry_right, union_continuousAt, union_of_isClosed, union_of_isOpen, comp, comp_inter, comp_inter_of_eq, comp_of_eq, comp_of_mem_nhdsWithin_image, comp_of_mem_nhdsWithin_image_of_eq, comp_of_preimage_mem_nhdsWithin, comp_of_preimage_mem_nhdsWithin_of_eq, congr_mono, congr_of_eventuallyEq, congr_of_eventuallyEq_insert, congr_of_eventuallyEq_of_mem, congr_of_insert, congr_of_mem, congr_set, continuousAt, diff_iff, finCons, finInsertNth, finSnoc, fst, image_closure, insert, matrixVecCons, mem_closure, mem_closure_image, mono, mono_of_mem_nhdsWithin, preimage_mem_nhdsWithin, preimage_mem_nhdsWithin', preimage_mem_nhdsWithin'', prodMap, prodMk, snd, tendsto, tendsto_nhdsWithin, tendsto_nhdsWithin_image, union, congr_continuousWithinAt, congr_continuousWithinAt_of_insert, congr_continuousWithinAt_of_mem, map_nhds_eq, continuousOn_iff, continuousOn_image_of_leftInvOn, continuousOn_range_of_leftInverse, map_nhdsWithin_eq, closure_of_continuousOn, closure_of_continuousWithinAt, continuousOn, continuousOn_iff, map_nhdsWithin_eq, continuousOn_iff, continuousOn_image_iff, continuousWithinAt_iff, map_nhdsWithin_eq, map_nhdsWithin_preimage_eq, continuousOn_isOpen_iff, antitone_continuousOn, continouousOn_union_iff_of_isClosed, continouousOn_union_iff_of_isOpen, continuousAt_of_not_accPt, continuousAt_of_not_accPt_top, continuousAt_prod_of_discrete_left, continuousAt_prod_of_discrete_right, continuousOn_apply, continuousOn_congr, continuousOn_const, continuousOn_empty, continuousOn_fst, continuousOn_iUnion_iff_of_isOpen, continuousOn_id, continuousOn_id', continuousOn_iff, continuousOn_iff', continuousOn_iff_continuous_restrict, continuousOn_iff_isClosed, continuousOn_isOpen_of_generateFrom, continuousOn_of_forall_continuousAt, continuousOn_of_locally_continuousOn, continuousOn_open_iff, continuousOn_pi, continuousOn_pi', continuousOn_prod_of_discrete_left, continuousOn_prod_of_discrete_right, continuousOn_singleton, continuousOn_snd, continuousOn_to_generateFrom_iff, continuousOn_union_iff_of_isClosed, continuousOn_union_iff_of_isOpen, continuousOn_univ, continuousWithinAt_compl_self, continuousWithinAt_congr, continuousWithinAt_congr_of_insert, continuousWithinAt_congr_of_mem, continuousWithinAt_congr_set, continuousWithinAt_const, continuousWithinAt_diff_self, continuousWithinAt_fst, continuousWithinAt_id, continuousWithinAt_iff_continuousAt, continuousWithinAt_iff_continuousAt_restrict, continuousWithinAt_insert_self, continuousWithinAt_inter, continuousWithinAt_inter', continuousWithinAt_of_notMem_closure, continuousWithinAt_of_not_accPt, continuousWithinAt_pi, continuousWithinAt_prod_iff, continuousWithinAt_prod_of_discrete_left, continuousWithinAt_prod_of_discrete_right, continuousWithinAt_singleton, continuousWithinAt_snd, continuousWithinAt_union, continuousWithinAt_univ, continuous_of_continuousOn_iUnion_of_isOpen, continuous_of_cover_nhds, continuous_prod_of_discrete_left, continuous_prod_of_discrete_right, isOpenMap_prod_of_discrete_left, isOpenMap_prod_of_discrete_right, nhdsWithin_le_comap	171
Total	172

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_continuousOn 📖	mathematical	Continuous ContinuousOn	ContinuousOn	—	ContinuousOn.comp continuousOn Set.mapsTo_univ
comp_continuousOn' 📖	mathematical	Continuous ContinuousOn	ContinuousOn	—	comp_continuousOn
continuousOn 📖	mathematical	Continuous	ContinuousOn	—	ContinuousOn.mono continuousOn_univ Set.subset_univ
continuousWithinAt 📖	mathematical	Continuous	ContinuousWithinAt	—	ContinuousAt.continuousWithinAt continuousAt
preimage_mem_nhdsSet 📖	mathematical	Continuous Set Filter Filter.instMembership nhdsSet	Set Filter Filter.instMembership nhdsSet Set.preimage	—	nhdsSetWithin_univ preimage_mem_nhdsSetWithin
preimage_mem_nhdsSetWithin 📖	mathematical	Continuous Set Filter Filter.instMembership nhdsSetWithin	Set Filter Filter.instMembership nhdsSetWithin Set.preimage	—	Set.univ_inter ContinuousOn.preimage_mem_nhdsSetWithin continuousOn
tendsto_nhdsSet 📖	mathematical	Continuous Set.MapsTo	Filter.Tendsto nhdsSet	—	ContinuousOn.tendsto_nhdsSet continuousOn Filter.univ_mem
tendsto_nhdsSet_nhds 📖	mathematical	Continuous Set.EqOn	Filter.Tendsto nhdsSet nhds	—	nhdsSet_singleton tendsto_nhdsSet

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_continuousWithinAt 📖	mathematical	ContinuousAt ContinuousWithinAt	ContinuousWithinAt	—	ContinuousWithinAt.comp continuousWithinAt Set.mapsTo_univ
comp_continuousWithinAt_of_eq 📖	mathematical	ContinuousAt ContinuousWithinAt	ContinuousWithinAt	—	comp_continuousWithinAt
comp₂_continuousWithinAt 📖	mathematical	ContinuousAt instTopologicalSpaceProd ContinuousWithinAt	ContinuousWithinAt	—	comp_continuousWithinAt Filter.Tendsto.prodMk_nhds
comp₂_continuousWithinAt_of_eq 📖	mathematical	ContinuousAt instTopologicalSpaceProd ContinuousWithinAt	ContinuousWithinAt	—	comp₂_continuousWithinAt
congr_of_eventuallyEq 📖	mathematical	ContinuousAt Filter.EventuallyEq nhds	ContinuousAt	—	congr Filter.EventuallyEq.symm
continuousWithinAt 📖	mathematical	ContinuousAt	ContinuousWithinAt	—	ContinuousWithinAt.mono continuousWithinAt_univ Set.subset_univ

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	ContinuousOn Set.MapsTo	ContinuousOn	—	ContinuousWithinAt.comp
comp' 📖	mathematical	ContinuousOn Set.MapsTo	ContinuousOn	—	comp
comp_continuous 📖	mathematical	ContinuousOn Continuous Set Set.instMembership	Continuous	—	continuousOn_univ comp
comp_inter 📖	mathematical	ContinuousOn	ContinuousOn Set Set.instInter Set.preimage	—	comp mono Set.inter_subset_left Set.inter_subset_right
congr_mono 📖	mathematical	ContinuousOn Set.EqOn Set Set.instHasSubset	ContinuousOn	—	ContinuousWithinAt.mono Filter.Tendsto.congr' Filter.EventuallyEq.symm Set.EqOn.eventuallyEq_nhdsWithin
continuousAt 📖	mathematical	ContinuousOn Set Filter Filter.instMembership nhds	ContinuousAt	—	ContinuousWithinAt.continuousAt mem_of_mem_nhds
continuousWithinAt 📖	mathematical	ContinuousOn Set Set.instMembership	ContinuousWithinAt	—	—
finCons 📖	mathematical	ContinuousOn Pi.topologicalSpace	ContinuousOn Pi.topologicalSpace Fin.cons	—	ContinuousWithinAt.finCons
finInsertNth 📖	mathematical	ContinuousOn Pi.topologicalSpace Fin.succAbove	ContinuousOn Pi.topologicalSpace Fin.insertNth	—	ContinuousWithinAt.finInsertNth
finSnoc 📖	mathematical	ContinuousOn Pi.topologicalSpace	ContinuousOn Pi.topologicalSpace Fin.snoc	—	ContinuousWithinAt.finSnoc
fst 📖	mathematical	ContinuousOn instTopologicalSpaceProd	ContinuousOn	—	Continuous.comp_continuousOn continuous_fst
iUnion_of_isOpen 📖	mathematical	ContinuousOn IsOpen	ContinuousOn Set.iUnion	—	ContinuousAt.continuousWithinAt continuousAt IsOpen.mem_nhds
image_closure 📖	mathematical	ContinuousOn closure	Set Set.instHasSubset Set.image closure	—	ContinuousWithinAt.image_closure ContinuousWithinAt.mono subset_closure
image_comp_continuous 📖	mathematical	ContinuousOn Set.image Continuous	ContinuousOn	—	comp Continuous.continuousOn Set.mapsTo_image
isOpen_inter_preimage 📖	mathematical	ContinuousOn IsOpen	IsOpen Set Set.instInter Set.preimage	—	continuousOn_open_iff
isOpen_preimage 📖	mathematical	ContinuousOn IsOpen Set Set.instHasSubset Set.preimage	IsOpen Set.preimage	—	Set.inter_comm Set.inter_eq_self_of_subset_left continuousOn_open_iff
iterate 📖	mathematical	ContinuousOn Set.MapsTo	ContinuousOn Nat.iterate	—	continuousOn_id comp
mapsToRestrict 📖	mathematical	ContinuousOn Set.MapsTo	Continuous Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	—	Continuous.codRestrict restrict
matrixVecCons 📖	mathematical	ContinuousOn Pi.topologicalSpace	ContinuousOn Pi.topologicalSpace Matrix.vecCons	—	ContinuousWithinAt.matrixVecCons
mono 📖	mathematical	ContinuousOn Set Set.instHasSubset	ContinuousOn	—	Filter.Tendsto.mono_left nhdsWithin_mono
mono_dom 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder ContinuousOn	ContinuousOn	—	Filter.map_mono inf_le_inf_right nhds_mono
mono_rng 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder ContinuousOn	ContinuousOn	—	nhds_mono
preimage_interior_subset_interior_preimage 📖	mathematical	ContinuousOn IsOpen	Set Set.instHasSubset Set.instInter Set.preimage interior	—	interior_maximal Set.inter_subset_inter Set.Subset.refl Set.preimage_mono interior_subset isOpen_inter_preimage isOpen_interior interior_inter IsOpen.interior_eq
preimage_isClosed_of_isClosed 📖	mathematical	ContinuousOn	IsClosed Set Set.instInter Set.preimage	—	continuousOn_iff_isClosed Set.inter_comm IsClosed.inter
preimage_mem_nhdsSetWithin 📖	mathematical	ContinuousOn Set Filter Filter.instMembership nhdsSetWithin	Set Filter Filter.instMembership nhdsSetWithin Set.instInter Set.preimage	—	mem_nhdsSetWithin continuousOn_iff' Eq.trans_subset Set.inter_comm HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_inter_left Set.preimage_mono Set.inter_subset_left Set.inter_assoc Set.preimage_inter Set.inter_subset_right
preimage_mem_nhdsSetWithin_of_mem_nhdsSet 📖	mathematical	ContinuousOn Set Filter Filter.instMembership nhdsSet	Set Filter Filter.instMembership nhdsSetWithin Set.instInter Set.preimage	—	nhdsSetWithin_univ Set.inter_univ preimage_mem_nhdsSetWithin
prodMap 📖	mathematical	ContinuousOn	ContinuousOn instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	ContinuousWithinAt.prodMap
prodMk 📖	mathematical	ContinuousOn	ContinuousOn instTopologicalSpaceProd	—	ContinuousWithinAt.prodMk
restrict 📖	mathematical	ContinuousOn	Continuous Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict	—	continuousOn_iff_continuous_restrict
snd 📖	mathematical	ContinuousOn instTopologicalSpaceProd	ContinuousOn	—	Continuous.comp_continuousOn continuous_snd
tendsto_nhdsSet 📖	mathematical	ContinuousOn Set Filter Filter.instMembership nhdsSet Set.MapsTo	Filter.Tendsto nhdsSet	—	mem_nhdsSet_iff_exists Filter.HasBasis.tendsto_iff hasBasis_nhdsSet isOpen_inter_preimage mono Set.subset_inter Set.MapsTo.mono Set.Subset.rfl Set.mem_preimage Set.mem_of_mem_inter_right
uncurry_left 📖	mathematical	Set Set.instMembership ContinuousOn instTopologicalSpaceProd SProd.sprod Set.instSProd	ContinuousOn	—	congr comp Continuous.continuousOn Continuous.prodMk continuous_const continuous_id'
uncurry_right 📖	mathematical	Set Set.instMembership ContinuousOn instTopologicalSpaceProd SProd.sprod Set.instSProd	ContinuousOn	—	congr comp Continuous.continuousOn Continuous.prodMk continuous_id' continuous_const
union_continuousAt 📖	mathematical	IsOpen ContinuousOn ContinuousAt	ContinuousOn Set Set.instUnion	—	continuousOn_of_forall_continuousAt ContinuousWithinAt.continuousAt continuousWithinAt IsOpen.mem_nhds
union_of_isClosed 📖	mathematical	ContinuousOn	ContinuousOn Set Set.instUnion	—	ContinuousWithinAt.union continuousWithinAt_of_notMem_closure IsClosed.closure_eq
union_of_isOpen 📖	mathematical	ContinuousOn IsOpen	ContinuousOn Set Set.instUnion	—	union_continuousAt IsOpen.continuousOn_iff

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	ContinuousWithinAt Set.MapsTo	ContinuousWithinAt	—	Filter.Tendsto.comp tendsto tendsto_nhdsWithin
comp_inter 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Set Set.instInter Set.preimage	—	comp mono Set.inter_subset_left Set.inter_subset_right
comp_inter_of_eq 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Set Set.instInter Set.preimage	—	comp_inter
comp_of_eq 📖	mathematical	ContinuousWithinAt Set.MapsTo	ContinuousWithinAt	—	comp
comp_of_mem_nhdsWithin_image 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.image	ContinuousWithinAt	—	comp mono_of_mem_nhdsWithin Set.mapsTo_image
comp_of_mem_nhdsWithin_image_of_eq 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.image	ContinuousWithinAt	—	comp_of_mem_nhdsWithin_image
comp_of_preimage_mem_nhdsWithin 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.preimage	ContinuousWithinAt	—	Filter.Tendsto.comp tendsto tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
comp_of_preimage_mem_nhdsWithin_of_eq 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.preimage	ContinuousWithinAt	—	comp_of_preimage_mem_nhdsWithin
congr_mono 📖	mathematical	ContinuousWithinAt Set.EqOn Set Set.instHasSubset	ContinuousWithinAt	—	congr mono
congr_of_eventuallyEq 📖	mathematical	ContinuousWithinAt Filter.EventuallyEq nhdsWithin	ContinuousWithinAt	—	Filter.EventuallyEq.congr_continuousWithinAt
congr_of_eventuallyEq_insert 📖	mathematical	ContinuousWithinAt Filter.EventuallyEq nhdsWithin Set Set.instInsert	ContinuousWithinAt	—	congr_of_eventuallyEq nhdsWithin_mono Set.subset_insert mem_of_mem_nhdsWithin Set.mem_insert
congr_of_eventuallyEq_of_mem 📖	mathematical	ContinuousWithinAt Filter.EventuallyEq nhdsWithin Set Set.instMembership	ContinuousWithinAt	—	congr_of_eventuallyEq mem_of_mem_nhdsWithin
congr_of_insert 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt	—	congr Set.mem_insert_of_mem Set.mem_insert
congr_of_mem 📖	mathematical	ContinuousWithinAt Set Set.instMembership	ContinuousWithinAt	—	congr
congr_set 📖	mathematical	ContinuousWithinAt Filter.EventuallyEq nhds	ContinuousWithinAt	—	continuousWithinAt_congr_set
continuousAt 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhds	ContinuousAt	—	continuousWithinAt_iff_continuousAt
diff_iff 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Set Set.instSDiff	—	mono union Set.diff_union_self Set.diff_subset
finCons 📖	mathematical	ContinuousWithinAt Pi.topologicalSpace	ContinuousWithinAt Pi.topologicalSpace Fin.cons	—	Filter.Tendsto.finCons tendsto
finInsertNth 📖	mathematical	ContinuousWithinAt Pi.topologicalSpace Fin.succAbove	ContinuousWithinAt Pi.topologicalSpace Fin.insertNth	—	Filter.Tendsto.finInsertNth tendsto
finSnoc 📖	mathematical	ContinuousWithinAt Pi.topologicalSpace	ContinuousWithinAt Pi.topologicalSpace Fin.snoc	—	Filter.Tendsto.finSnoc tendsto
fst 📖	mathematical	ContinuousWithinAt instTopologicalSpaceProd	ContinuousWithinAt	—	ContinuousAt.comp_continuousWithinAt continuousAt_fst
image_closure 📖	mathematical	ContinuousWithinAt	Set Set.instHasSubset Set.image closure	—	Set.MapsTo.image_subset Set.MapsTo.closure_of_continuousWithinAt Set.mapsTo_image
insert 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Set Set.instInsert	—	continuousWithinAt_insert_self
matrixVecCons 📖	mathematical	ContinuousWithinAt Pi.topologicalSpace	ContinuousWithinAt Pi.topologicalSpace Matrix.vecCons	—	Filter.Tendsto.matrixVecCons tendsto
mem_closure 📖	mathematical	ContinuousWithinAt Set Set.instMembership closure Set.MapsTo	Set Set.instMembership closure	—	closure_mono Set.image_subset_iff mem_closure_image
mem_closure_image 📖	mathematical	ContinuousWithinAt Set Set.instMembership closure	Set Set.instMembership closure Set.image	—	mem_closure_of_tendsto mem_closure_iff_nhdsWithin_neBot Filter.mem_of_superset self_mem_nhdsWithin Set.subset_preimage_image
mono 📖	mathematical	ContinuousWithinAt Set Set.instHasSubset	ContinuousWithinAt	—	Filter.Tendsto.mono_left nhdsWithin_mono
mono_of_mem_nhdsWithin 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin	ContinuousWithinAt	—	Filter.Tendsto.mono_left nhdsWithin_le_of_mem
preimage_mem_nhdsWithin 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhds	Set Filter Filter.instMembership nhdsWithin Set.preimage	—	—
preimage_mem_nhdsWithin' 📖	mathematical	ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.image	Set Filter Filter.instMembership nhdsWithin Set.preimage	—	tendsto_nhdsWithin Set.mapsTo_image
preimage_mem_nhdsWithin'' 📖	mathematical	ContinuousWithinAt Set.preimage Set Filter Filter.instMembership nhdsWithin	Set Filter Filter.instMembership nhdsWithin Set.preimage	—	preimage_mem_nhdsWithin' nhdsWithin_mono Set.image_preimage_subset
prodMap 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	prodMk comp continuousWithinAt_fst Set.mapsTo_fst_prod continuousWithinAt_snd Set.mapsTo_snd_prod
prodMk 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt instTopologicalSpaceProd	—	Filter.Tendsto.prodMk_nhds
snd 📖	mathematical	ContinuousWithinAt instTopologicalSpaceProd	ContinuousWithinAt	—	ContinuousAt.comp_continuousWithinAt continuousAt_snd
tendsto 📖	mathematical	ContinuousWithinAt	Filter.Tendsto nhdsWithin nhds	—	—
tendsto_nhdsWithin 📖	mathematical	ContinuousWithinAt Set.MapsTo	Filter.Tendsto nhdsWithin	—	Filter.tendsto_inf Filter.tendsto_principal Filter.mem_inf_of_right Filter.mem_principal
tendsto_nhdsWithin_image 📖	mathematical	ContinuousWithinAt	Filter.Tendsto nhdsWithin Set.image	—	tendsto_nhdsWithin Set.mapsTo_image
union 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt Set Set.instUnion	—	continuousWithinAt_union

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_continuousWithinAt 📖	mathematical	Filter.EventuallyEq nhdsWithin	ContinuousWithinAt	—	ContinuousWithinAt.eq_1 Filter.tendsto_congr'
congr_continuousWithinAt_of_insert 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instInsert	ContinuousWithinAt	—	ContinuousWithinAt.congr_of_eventuallyEq_insert symm
congr_continuousWithinAt_of_mem 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instMembership	ContinuousWithinAt	—	ContinuousWithinAt.congr_of_eventuallyEq_of_mem symm

Function.LeftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_nhds_eq 📖	mathematical	ContinuousWithinAt Set.range ContinuousAt	Filter.map nhds nhdsWithin Set.range	—	nhdsWithin_univ Set.image_univ Set.LeftInvOn.map_nhdsWithin_eq leftInvOn ContinuousAt.continuousWithinAt

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_iff 📖	mathematical	IsOpen	ContinuousOn ContinuousAt	—	continuousWithinAt_iff_continuousAt mem_nhds

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_image_of_leftInvOn 📖	mathematical	IsOpenMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict Set.LeftInvOn	ContinuousOn Set.image	—	continuousOn_iff' Set.image_restrict IsOpen.preimage continuous_subtype_val Set.inter_eq_self_of_subset_left Set.image_mono Set.inter_subset_right Set.LeftInvOn.image_inter'
continuousOn_range_of_leftInverse 📖	mathematical	IsOpenMap	ContinuousOn Set.range	—	Set.image_univ continuousOn_image_of_leftInvOn restrict isOpen_univ

Set.LeftInvOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_nhdsWithin_eq 📖	mathematical	Set.LeftInvOn ContinuousWithinAt Set.image	Filter.map nhdsWithin Set.image	—	le_antisymm ContinuousWithinAt.tendsto_nhdsWithin Set.mapsTo_image Set.EqOn.eventuallyEq_of_mem Set.RightInvOn.eqOn rightInvOn_image self_mem_nhdsWithin Filter.le_map_of_right_inverse mapsTo Set.surjOn_image

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_of_continuousOn 📖	mathematical	Set.MapsTo ContinuousOn closure	Set.MapsTo closure	—	closure_of_continuousWithinAt ContinuousWithinAt.mono subset_closure
closure_of_continuousWithinAt 📖	mathematical	Set.MapsTo ContinuousWithinAt	Set.MapsTo closure	—	ContinuousWithinAt.mem_closure

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	mathematical	Set.Subsingleton	ContinuousOn	—	induction_on continuousOn_empty continuousOn_singleton

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_iff 📖	mathematical	Topology.IsEmbedding	ContinuousOn	—	Topology.IsInducing.continuousOn_iff isInducing
map_nhdsWithin_eq 📖	mathematical	Topology.IsEmbedding	Filter.map nhdsWithin Set.image	—	Topology.IsInducing.map_nhdsWithin_eq isInducing

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_iff 📖	mathematical	Topology.IsInducing	ContinuousOn	—	continuousWithinAt_iff
continuousOn_image_iff 📖	mathematical	Topology.IsInducing	ContinuousOn Set.image	—	map_nhdsWithin_eq
continuousWithinAt_iff 📖	mathematical	Topology.IsInducing	ContinuousWithinAt	—	tendsto_nhds_iff
map_nhdsWithin_eq 📖	mathematical	Topology.IsInducing	Filter.map nhdsWithin Set.image	—	Filter.ext nhds_eq_comap

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_nhdsWithin_preimage_eq 📖	mathematical	Topology.IsOpenEmbedding	Filter.map nhdsWithin Set.preimage	—	Topology.IsEmbedding.map_nhdsWithin_eq isEmbedding Set.image_preimage_eq_inter_range nhdsWithin_eq_nhdsWithin Set.mem_range_self isOpen_range Set.inter_assoc Set.inter_self

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_isOpen_iff 📖	mathematical	Topology.IsQuotientMap IsOpen	ContinuousOn Set.preimage	—	continuous_iff restrictPreimage_isOpen

(root)

Definitions

Name	Category	Theorems
ContinuousOn 📖	MathDef	448 math math: ContinuousOn.clm_apply, continuousOn_ceil, cfcₙ_def, Real.continuousOn_rpowIntegrand₀₁_uncurry, AnalyticOn.continuousOn, ContinuousOn.rpow, continuousOn_stereoToFun, Complex.continuousOn_exp, intervalIntegral.continuousOn_primitive_interval, ConvexOn.continuousOn_tfae, Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure, ContinuousOn.div_const, ContinuousOn.finset_inf'_apply, continuousOn_of_uniform_approx_of_continuousOn, Set.Subsingleton.continuousOn, ContinuousOn.enatSub, ApproximatesLinearOn.inverse_continuousOn, WithTop.continuousOn_untopD, continuousOn_tsum, mdifferentiableOn_iff, ContinuousOn.uncurry_left, continuousOn_union_iff_of_isClosed, continuousOn_boolIndicator_iff_isClopen, ChartedSpaceCore.continuousOn_toFun, continuousOn_prod_of_discrete_right, antitone_continuousOn, DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv, ContinuousOn.neg, Uniform.continuousOn_iff'_left, continuousOn_dslope, continuousOn_floor, HasGradientAt.continuousOn, Topology.RelCWComplex.continuousOn_symm, ContinuousOn.fun_mul, Topology.CWComplex.continuousOn, ContinuousOn.add_const, Complex.continuousOn_arg, ContinuousOn.matrixVecCons, ContinuousOn.eval_const, Unitary.continuousOn_argSelfAdjoint, OpenPartialHomeomorph.continuousOn_univBall_symm, continuousOn_neg, ContinuousOn.cfcₙ', Continuous.continuousOn, ContinuousOn.of_inv, ContinuousOn.finCons, Real.ContinuousOn.circleAverage, ContinuousAlgEquiv.continuousOn, contDiffOn_iff_continuousOn_differentiableOn, FiberPrebundle.continuous_trivChange, IsOpenMap.continuousOn_range_of_leftInverse, ContinuousOn.image_comp_continuous, MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iio, IsOpen.continuousOn_iff, continuousOn_Icc_extendFrom_Ioo, DifferentiableOn.continuousOn, ContinuousOn.const_add, FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas, intervalIntegral.continuousOn_primitive, continuousOn_fract, HasDerivAt.continuousOn, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, Complex.continuousOn_cos, Bundle.Trivialization.Prod.continuous_inv_fun, continuousOn_of_forall_continuousAt, Continuous.comp_continuousOn, ContinuousOn.vadd, continuousOn_star, intervalIntegral.continuousOn_primitive_interval_left, continuousOn_iUnion_iff_of_isOpen, CFC.continuousOn_log, Topology.RelCWComplex.continuousOn, Real.continuousOn_log, ContinuousOn.cfc_nnreal', ContinuousOn.finset_inf_apply, LipschitzOnWith.continuousOn, ContinuousOn.sup, continuousOn_zpow, continuousOn_integral_of_compact_support, ContinuousOn.log, ContinuousOn.cfc, continuousOn_congr, ENNReal.continuousOn_sub, CFC.continuousOn_sqrt, ContinuousOn.logb, ContinuousOn.mul_const, ODE.FunSpace.continuousOn_comp_compProj, Topology.IsCoherentWith.continuous_iff, ContDiffOn.continuousOn_iteratedDerivWithin, continuousOn_iff, continuousOn_singleton, ContinuousOn.ereal_toENNReal, ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux', ContinuousOn.finset_inf, contDiffAt_one_iff, MDifferentiableOn.continuousOn, MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ici, contDiffOn_one_iff_derivWithin, ContinuousOn.union_continuousAt, ContinuousOn.clm_comp, continuousOn_tangentCoordChange, ContinuousOn.fun_add, mdifferentiableOn_iff_target, lipschitzOnWith_cfc_fun_of_subset, ContinuousOn.sub, continuousOn_cfc_setProd, IsometryEquiv.comp_continuousOn_iff, AffineIsometryEquiv.continuousOn, MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iic, ContDiffOn.continuousOn_iteratedFDerivWithin, continuousOn_cfcₙ, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith', contDiffWithinAt_zero, HasFTaylorSeriesUpToOn.cont, IsPicardLindelof.continuousOn, continouousOn_union_iff_of_isClosed, ContinuousOn.mono_dom, MeasureTheory.continuousOn_of_dominated, ContinuousOn.norm', contDiffOn_nat_iff_continuousOn_differentiableOn, Complex.continuousOn_sin, HurwitzZeta.continuousOn_cosKernel, ContinuousOn.inv, ContinuousOn.lineMap, continuousOn_zsmul, ContinuousOn.finset_sup', ContinuousOn.of_dslope, continuousOn_const, ContinuousOn.inversion, ContinuousMap.continuousOn_mkD_of_uncurry, ConcaveOn.continuousOn, intervalIntegral.continuousOn_primitive_Icc, ContinuousOn.union_of_isClosed, ContinuousOn.finset_inf', continuousOn_cfc_nnreal, ContDiffOn.continuousOn_zero, ContinuousOn.iUnion_of_isOpen, hasFTaylorSeriesUpToOn_zero_iff, Polynomial.continuousOn, ContinuousOn.iterate, Complex.continuousOn_norm_circleTransformBoundingFunction, ContinuousOn.prodMap, continuousOn_pow, continuousOn_extChartAt, SeparationQuotient.continuousOn_lift, Units.continuousOn_zpow₀_spectrum, TendstoLocallyUniformlyOn.continuousOn, ZetaAsymptotics.continuousOn_term, continuousOn_piecewise_ite', ContinuousOn.snd, continuousOn_inv, ContinuousOn.clm_bundle_apply₂, Set.EquicontinuousOn.continuousOn_of_mem, ContinuousOn.ennreal_mul, ContinuousOn.finset_sup_apply, continuousOn_extendFrom, Real.continuousOn_cos, cfc_def, HasFPowerSeriesWithinOnBall.continuousOn, continuousOn_prod_of_continuousOn_lipschitzOnWith, ContMDiffOn.continuousOn_tangentMapWithin, continuousOn_piecewise_ite, Uniform.continuousOn_iff'_right, equicontinuousOn_iff_continuousOn, DiffContOnCl.continuousOn_ball, IsLocalHomeomorphOn.continuousOn, HurwitzZeta.continuousOn_evenKernel, MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ioi, OpenPartialHomeomorph.continuousOn_extend_symm, MeasureTheory.continuousOn_convolution_right_with_param_comp, Real.continuousOn_logb, lipschitzOnWith_cfc_fun, ContinuousOn.cpow_const, Bundle.Trivialization.continuousOn_symm, ContinuousOn.nsmul, Filter.Tendsto.continuousOn_of_equicontinuousOn, BoxIntegral.Box.continuousOn_face_Icc, ContinuousOn.zsmul, IsPicardLindelof.continuousOn_uncurry, continuousOn_div, ENNReal.continuousOn_sub_left, Bundle.Pretrivialization.continuousOn_continuousLinearMapCoordChange, continuousOn_inv₀, InnerProductSpace.HarmonicOnNhd.continuousOn, ContinuousOn.piecewise, ContinuousOn.div, contDiffOn_zero, HurwitzZeta.continuousOn_oddKernel, ContinuousOn.cfc_nnreal_of_mem_nhdsSet, VectorBundle.continuousOn_coordChange', continuousOn_iff_lower_upperSemicontinuousOn, HurwitzZeta.continuousOn_sinKernel, OpenPartialHomeomorph.continuousOn_writtenInExtend_iff, mdifferentiableOn_iff_of_subset_source, EReal.continuousOn_toReal, LocallyLipschitzOn.continuousOn, HasFTaylorSeriesUpToOn.continuousOn, ContinuousOn.union_of_isOpen, continuousOn_apply, CFC.continuousOn_nnrpow, continuousOn_update_iff, ContinuousMap.continuousOn_of_continuousOn_uncurry, ContinuousOn.continuousOn_iteratedFDerivWithin, UniformContinuousOn.continuousOn, ContMDiffOn.continuousOn, lipschitzOnWith_cfcₙ_fun, ContinuousOn.prod_mapL, continuousOn_uIcc_extendFrom_uIoo, ContinuousLinearEquiv.comp_continuousOn_iff, ContinuousOn.if', ContinuousOn.coeFun, Real.continuousOn_exp, continuousOn_const_smul_iff₀, ContinuousOn.sqrt, ContinuousOn.comp', continuousOn_isOpen_of_generateFrom, continuousOn_union_iff_of_isOpen, ContinuousOn.cfc_nnreal, ContDiffOn.continuousOn_fderivWithin_apply, Topology.IsEmbedding.continuousOn_iff, InnerProductSpace.HarmonicContOnCl.continuousOn_ball, Dilation.comp_continuousOn_iff, ContinuousOn.finset_sup'_apply, OpenPartialHomeomorph.continuousOn_invFun, ContinuousOn.comp_inter, Homeomorph.comp_continuousOn_iff, ContinuousOn.inf', Complex.continuousOn_tan, ContinuousOn.comp, UniformOnFun.continuousOn_eval₂, ContDiffOn.continuousOn_derivWithin, ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet, Real.continuousOn_sin, continuousOn_snd, ContinuousOn.cfc_of_mem_nhdsSet, ContDiffOn.continuousOn_fderivWithin, ContinuousOn.partialSups, AnalyticOnNhd.continuousOn, HasFiniteFPowerSeriesOnBall.continuousOn, Set.Finite.continuousOn, ContinuousOn.arcsin, continuousOn_fst, NNReal.continuousOn_rpow_const, VectorPrebundle.exists_coordChange, ContinuousOn.abs, ContinuousOn.congr, ConvexOn.locallyLipschitzOn_iff_continuousOn, ContinuousOn.cfcₙ_fun, continuousOn_inv_iff, ContinuousOn.nnnorm, Complex.continuousOn_prod_circle_transform_function, ModelWithCorners.continuousOn_symm, ContinuousOn.cfcₙ_nnreal', Bundle.Trivialization.continuousOn_proj, ContinuousOn.nnnorm', Real.continuousOn_rpowIntegrand₀₁_Ici, ContinuousOn.of_neg, ContDiffOn.continuousOn_fderiv_of_isOpen, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn, contMDiffOn_iff, ConcaveOn.continuousOn_interior, ContinuousOn.fst, ENNReal.continuousOn_toNNReal, IsIntegralCurveOn.continuousOn, ContinuousOn.finset_sup, CPolynomialOn.continuousOn, continuousOn_extChartAt_symm, ContinuousOn.ofReal_map_toNNReal, ContinuousOn.mono_rng, ContinuousOn.cfcₙ, ContinuousOn.angle_sign_comp, continuousOn_const_smul_iff, Isometry.comp_continuousOn_iff, Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, OpenPartialHomeomorph.continuousOn, DiffContOnCl.continuousOn, ContinuousOn.zpow₀, lipschitzOnWith_cfcₙ_fun_of_subset, ContinuousOn.cfcₙ_of_mem_nhdsSet, continuousOn_empty, continuousOn_iff_continuous_restrict, ContinuousOn.compCM, continuousOn_multiset_prod, continuousOn_prod_of_continuousOn_lipschitzOnWith', ZetaAsymptotics.continuousOn_term_tsum, ContinuousOn.arsinh, ContinuousOn.congr_mono, contMDiffOn_iff_of_mem_maximalAtlas, ContinuousOn.smul, Units.continuousOn_inv₀_spectrum, IsUnit.continuousOn_const_smul_iff, continuousOn_nsmul, ContinuousOn.arccos, ContinuousMap.continuousOn_mkD_restrict_of_uncurry, ContinuousOn.cfc', continuousOn_Ioc_extendFrom_Ioo, MeasureTheory.continuousOn_convolution_right_with_param, VectorBundleCore.continuousOn_coordChange, LinearIsometryEquiv.continuousOn, Bundle.Trivialization.Prod.continuous_to_fun, hasFTaylorSeriesUpToOn_succ_iff_left, ContDiffOn.continuousOn, Bundle.Trivialization.continuousOn, ContinuousOn.prodMk, ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux, ContinuousOn.cfc_fun, ContinuousOn.inf, contMDiffOn_iff_of_subset_source, ContinuousOn.star, continuousOn_cfcₙ_nnreal, ContinuousOn.inv₀, ContinuousOn.finSnoc, continuousOn_prod_of_discrete_left, equicontinuousOn_unique, continuousOn_iff_isClosed, LinearIsometryEquiv.comp_continuousOn_iff, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support, VectorPrebundle.continuousOn_coordChange, upperHemicontinuousOn_singleton_iff, Real.continuousOn_tan, contDiffAt_zero, continuousOn_cfcₙ_setProd, ContinuousOn.const_cpow, ContinuousOn.mono, continuousOn_toIocDiv, OpenPartialHomeomorph.continuousOn_toFun, NormedSpace.continuousOn_exp, ConvexOn.continuousOn_interior, ContinuousOn.norm, continuousOn_finset_prod, ContinuousOn.div', ContinuousOn.partialSups_apply, NNReal.continuousOn_rpow_const_compl_zero, continuousOn_id', ContinuousOn.const_mul, ContinuousOn.div₀, HasFPowerSeriesOnBall.continuousOn, ContinuousOn.enorm, ContinuousOn.inner, ConcaveOn.continuousOn_tfae, continuousOn_Ico_extendFrom_Ioo, ContinuousOn.piecewise', IsMIntegralCurveOn.continuousOn, continuousOn_pi', OpenPartialHomeomorph.continuousOn_symm, ApproximatesLinearOn.continuousOn, continuousOn_of_locally_continuousOn, MeasureTheory.continuousOn_setToFun_of_dominated, continuousOn_open_iff, FiberBundleCore.continuousOn_coordChange, continuousOn_toIcoDiv, ContinuousOn.vsub, AffineIsometryEquiv.comp_continuousOn_iff, ContinuousOn.add, HasDerivWithinAt.continuousOn, ContinuousOn.cfcₙ_nnreal, ContinuousOn.sup', ContinuousOn.cpow, Complex.continuousOn_sqrt, ContinuousOn.clog, ENNReal.continuousOn_toReal, ContDiffOn.continuousOn_deriv_of_isOpen, continuousOn_iff', ContinuousOn.rpow_const, SeparationQuotient.continuousOn_lift₂, Topology.IsInducing.continuousOn_iff, Metric.continuousOn_iff', continuousOn_cfc_nnreal_setProd, IsOpenMap.continuousOn_image_of_leftInvOn, continuousOn_cfc, intervalIntegral.continuousOn_primitive_interval', continuousOn_id, continuousOn_univ, ContinuousOn.continuousOn_iteratedFDeriv, WithTop.continuousOn_untopA, OpenPartialHomeomorph.continuousOn_extend, TendstoUniformlyOn.continuousOn, continuousOn_taylorWithinEval, ContinuousOn.nhds, continuousOn_zpow₀, Continuous.comp_continuousOn', Real.continuousOn_rpowIntegrand₀₁, ContinuousOn.rexp, ContinuousOn.mul, Metric.continuousOn_iff, ContinuousOn.zpow, ContinuousOn.uncurry_right, Real.continuousOn_arcosh, continuousOn_to_generateFrom_iff, ODE.continuousOn_comp, ContinuousOn.const_smul, contMDiffOn_iff_target, Topology.IsInducing.continuousOn_image_iff, continuousOn_of_locally_uniform_approx_of_continuousWithinAt, ContinuousOn.if, ContinuousOn.inner_bundle, LocallyFinite.continuousOn_iUnion, contDiffOn_iff_continuousOn_differentiableOn_deriv, contMDiffOn_zero_iff, Topology.CWComplex.continuousOn_symm, continuousOn_cfcₙ_nnreal_setProd, ContinuousLinearEquiv.continuousOn, continuousOn_list_sum, CFC.continuousOn_rpow, ProbabilityTheory.continuousOn_mgf, FormalMultilinearSeries.continuousOn, OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_right, AbsolutelyContinuousOnInterval.continuousOn, continuousOn_clm_apply, IsLocalHomeomorph.exists_lift_nhds, HolderOnWith.continuousOn, EquicontinuousOn.continuousOn, Topology.IsQuotientMap.continuousOn_isOpen_iff, ContinuousOn.compMeasurePreservingLp, continuousOn_neg_iff, continuousOn_pi, Polynomial.continuousOn_aeval, ContinuousSqrt.continuousOn_sqrt, ContinuousOn.clm_bundle_apply, mdifferentiableOn_iff_of_mem_maximalAtlas, continuousOn_finset_sum, ContinuousOn.continuousLinearMapCoprod, OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left, continuousOn_multiset_sum, ContinuousOn.prod_map_equivL, continuousOn_coordChange, IsCoveringMapOn.continuousOn, DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁, ConcaveOn.locallyLipschitzOn_iff_continuousOn, LocallyFinite.continuousOn_iUnion', continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith, ConvexOn.continuousOn, ContinuousOn.finInsertNth, ContinuousOn.eval, Complex.continuousOn_one_add_mul_inv, continuousOn_const_vadd_iff, ContinuousOn.mabs, ContinuousOn.const_vadd, equicontinuousOn_finite, ContinuousOn.cexp, continuousOn_list_prod, ContinuousOn.pow, InnerProductSpace.HarmonicContOnCl.continuousOn, Real.continuousOn_tan_Ioo, continouousOn_union_iff_of_isOpen, unitary.continuousOn_argSelfAdjoint, FiberPrebundle.continuousOn_of_comp_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_continuousOn 📖	mathematical	—	Antitone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Prop.partialOrder ContinuousOn	—	ContinuousOn.mono
continouousOn_union_iff_of_isClosed 📖	mathematical	—	ContinuousOn Set Set.instUnion	—	continuousOn_union_iff_of_isClosed
continouousOn_union_iff_of_isOpen 📖	mathematical	IsOpen	ContinuousOn Set Set.instUnion	—	continuousOn_union_iff_of_isOpen
continuousAt_of_not_accPt 📖	mathematical	AccPt Filter.principal Compl.compl Set Set.instCompl Set.instSingletonSet	ContinuousAt	—	continuousWithinAt_compl_self continuousWithinAt_of_not_accPt
continuousAt_of_not_accPt_top 📖	mathematical	AccPt Top.top Filter Filter.instTop	ContinuousAt	—	continuousAt_of_not_accPt AccPt.mono
continuousAt_prod_of_discrete_left 📖	mathematical	—	ContinuousAt instTopologicalSpaceProd	—	continuousWithinAt_prod_of_discrete_left
continuousAt_prod_of_discrete_right 📖	mathematical	—	ContinuousAt instTopologicalSpaceProd	—	continuousWithinAt_prod_of_discrete_right
continuousOn_apply 📖	mathematical	—	ContinuousOn Pi.topologicalSpace	—	Continuous.continuousOn continuous_apply
continuousOn_congr 📖	mathematical	Set.EqOn	ContinuousOn	—	ContinuousOn.congr Set.EqOn.symm
continuousOn_const 📖	mathematical	—	ContinuousOn	—	Continuous.continuousOn continuous_const
continuousOn_empty 📖	mathematical	—	ContinuousOn Set Set.instEmptyCollection	—	—
continuousOn_fst 📖	mathematical	—	ContinuousOn instTopologicalSpaceProd	—	Continuous.continuousOn continuous_fst
continuousOn_iUnion_iff_of_isOpen 📖	mathematical	IsOpen	ContinuousOn Set.iUnion	—	ContinuousOn.mono Set.subset_iUnion_of_subset ContinuousOn.iUnion_of_isOpen
continuousOn_id 📖	mathematical	—	ContinuousOn	—	Continuous.continuousOn continuous_id
continuousOn_id' 📖	mathematical	—	ContinuousOn	—	continuousOn_id
continuousOn_iff 📖	mathematical	—	ContinuousOn Set IsOpen Set.instMembership Set.instHasSubset Set.instInter Set.preimage	—	—
continuousOn_iff' 📖	mathematical	—	ContinuousOn Set IsOpen Set.instInter Set.preimage	—	isOpen_induced_iff Set.restrict_eq Set.preimage_comp Set.inter_comm continuousOn_iff_continuous_restrict continuous_def
continuousOn_iff_continuous_restrict 📖	mathematical	—	ContinuousOn Continuous Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict	—	ContinuousOn.eq_1 continuous_iff_continuousAt continuousWithinAt_iff_continuousAt_restrict
continuousOn_iff_isClosed 📖	mathematical	—	ContinuousOn Set IsClosed Set.instInter Set.preimage	—	isClosed_induced_iff Set.restrict_eq Set.preimage_comp Set.inter_comm continuousOn_iff_continuous_restrict continuous_iff_isClosed
continuousOn_isOpen_of_generateFrom 📖	mathematical	IsOpen Set Set.instInter Set.preimage	ContinuousOn TopologicalSpace.generateFrom	—	continuousOn_to_generateFrom_iff mem_nhdsWithin
continuousOn_of_forall_continuousAt 📖	mathematical	ContinuousAt	ContinuousOn	—	ContinuousAt.continuousWithinAt
continuousOn_of_locally_continuousOn 📖	mathematical	Set IsOpen Set.instMembership ContinuousOn Set.instInter	ContinuousOn	—	nhdsWithin_restrict ContinuousWithinAt.eq_1
continuousOn_open_iff 📖	mathematical	IsOpen	ContinuousOn IsOpen Set Set.instInter Set.preimage	—	continuousOn_iff' Set.inter_comm IsOpen.inter Set.inter_assoc Set.inter_self
continuousOn_pi 📖	mathematical	—	ContinuousOn Pi.topologicalSpace	—	tendsto_pi_nhds
continuousOn_pi' 📖	mathematical	ContinuousOn	ContinuousOn Pi.topologicalSpace	—	continuousOn_pi
continuousOn_prod_of_discrete_left 📖	mathematical	—	ContinuousOn instTopologicalSpaceProd setOf Set Set.instMembership	—	—
continuousOn_prod_of_discrete_right 📖	mathematical	—	ContinuousOn instTopologicalSpaceProd setOf Set Set.instMembership	—	—
continuousOn_singleton 📖	mathematical	—	ContinuousOn Set Set.instSingletonSet	—	nhdsWithin_singleton mem_of_mem_nhds
continuousOn_snd 📖	mathematical	—	ContinuousOn instTopologicalSpaceProd	—	Continuous.continuousOn continuous_snd
continuousOn_to_generateFrom_iff 📖	mathematical	—	ContinuousOn TopologicalSpace.generateFrom Set Filter Filter.instMembership nhdsWithin Set.preimage	—	TopologicalSpace.nhds_generateFrom
continuousOn_union_iff_of_isClosed 📖	mathematical	—	ContinuousOn Set Set.instUnion	—	ContinuousOn.mono Set.subset_union_left Set.subset_union_right ContinuousOn.union_of_isClosed
continuousOn_union_iff_of_isOpen 📖	mathematical	IsOpen	ContinuousOn Set Set.instUnion	—	ContinuousOn.mono Set.subset_union_left Set.subset_union_right ContinuousOn.union_of_isOpen
continuousOn_univ 📖	mathematical	—	ContinuousOn Set.univ Continuous	—	nhdsWithin_univ
continuousWithinAt_compl_self 📖	mathematical	—	ContinuousWithinAt Compl.compl Set Set.instCompl Set.instSingletonSet ContinuousAt	—	Set.compl_eq_univ_diff continuousWithinAt_diff_self continuousWithinAt_univ
continuousWithinAt_congr 📖	mathematical	—	ContinuousWithinAt	—	ContinuousWithinAt.congr
continuousWithinAt_congr_of_insert 📖	mathematical	—	ContinuousWithinAt	—	continuousWithinAt_congr Set.mem_insert_of_mem Set.mem_insert
continuousWithinAt_congr_of_mem 📖	mathematical	Set Set.instMembership	ContinuousWithinAt	—	continuousWithinAt_congr
continuousWithinAt_congr_set 📖	mathematical	Filter.EventuallyEq nhds	ContinuousWithinAt	—	nhdsWithin_eq_iff_eventuallyEq
continuousWithinAt_const 📖	mathematical	—	ContinuousWithinAt	—	Continuous.continuousWithinAt continuous_const
continuousWithinAt_diff_self 📖	mathematical	—	ContinuousWithinAt Set Set.instSDiff Set.instSingletonSet	—	ContinuousWithinAt.diff_iff continuousWithinAt_singleton
continuousWithinAt_fst 📖	mathematical	—	ContinuousWithinAt instTopologicalSpaceProd	—	Continuous.continuousWithinAt continuous_fst
continuousWithinAt_id 📖	mathematical	—	ContinuousWithinAt	—	Continuous.continuousWithinAt continuous_id
continuousWithinAt_iff_continuousAt 📖	mathematical	Set Filter Filter.instMembership nhds	ContinuousWithinAt ContinuousAt	—	Set.univ_inter continuousWithinAt_inter continuousWithinAt_univ
continuousWithinAt_iff_continuousAt_restrict 📖	mathematical	Set Set.instMembership	ContinuousWithinAt ContinuousAt Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict	—	tendsto_nhdsWithin_iff_subtype
continuousWithinAt_insert_self 📖	mathematical	—	ContinuousWithinAt Set Set.instInsert	—	—
continuousWithinAt_inter 📖	mathematical	Set Filter Filter.instMembership nhds	ContinuousWithinAt Set Set.instInter	—	nhdsWithin_restrict'
continuousWithinAt_inter' 📖	mathematical	Set Filter Filter.instMembership nhdsWithin	ContinuousWithinAt Set Set.instInter	—	nhdsWithin_restrict''
continuousWithinAt_of_notMem_closure 📖	mathematical	Set Set.instMembership closure	ContinuousWithinAt	—	ContinuousWithinAt.eq_1 Filter.not_neBot mem_closure_iff_nhdsWithin_neBot Filter.tendsto_bot
continuousWithinAt_of_not_accPt 📖	mathematical	AccPt Filter.principal	ContinuousWithinAt	—	continuousWithinAt_diff_self Set.inter_comm
continuousWithinAt_pi 📖	mathematical	—	ContinuousWithinAt Pi.topologicalSpace	—	tendsto_pi_nhds
continuousWithinAt_prod_iff 📖	mathematical	—	ContinuousWithinAt instTopologicalSpaceProd	—	ContinuousWithinAt.fst ContinuousWithinAt.snd ContinuousWithinAt.prodMk
continuousWithinAt_prod_of_discrete_left 📖	mathematical	—	ContinuousWithinAt instTopologicalSpaceProd setOf Set Set.instMembership	—	nhds_prod_eq nhds_discrete Filter.pure_prod
continuousWithinAt_prod_of_discrete_right 📖	mathematical	—	ContinuousWithinAt instTopologicalSpaceProd setOf Set Set.instMembership	—	nhds_prod_eq nhds_discrete Filter.prod_pure
continuousWithinAt_singleton 📖	mathematical	—	ContinuousWithinAt Set Set.instSingletonSet	—	nhdsWithin_singleton
continuousWithinAt_snd 📖	mathematical	—	ContinuousWithinAt instTopologicalSpaceProd	—	Continuous.continuousWithinAt continuous_snd
continuousWithinAt_union 📖	mathematical	—	ContinuousWithinAt Set Set.instUnion	—	nhdsWithin_union
continuousWithinAt_univ 📖	mathematical	—	ContinuousWithinAt Set.univ ContinuousAt	—	ContinuousAt.eq_1 ContinuousWithinAt.eq_1 nhdsWithin_univ
continuous_of_continuousOn_iUnion_of_isOpen 📖	mathematical	ContinuousOn IsOpen Set.iUnion Set.univ	Continuous	—	continuousOn_univ ContinuousOn.iUnion_of_isOpen
continuous_of_cover_nhds 📖	mathematical	Set Filter Filter.instMembership nhds ContinuousOn	Continuous	—	continuous_iff_continuousAt ContinuousAt.eq_1 nhdsWithin_eq_nhds mem_of_mem_nhds
continuous_prod_of_discrete_left 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	continuousOn_prod_of_discrete_left
continuous_prod_of_discrete_right 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	continuousOn_prod_of_discrete_right
isOpenMap_prod_of_discrete_left 📖	mathematical	—	IsOpenMap instTopologicalSpaceProd	—	nhds_prod_eq nhds_discrete Filter.pure_prod Filter.map_map
isOpenMap_prod_of_discrete_right 📖	mathematical	—	IsOpenMap instTopologicalSpaceProd	—	nhds_prod_eq nhds_discrete Filter.prod_pure Filter.map_map
nhdsWithin_le_comap 📖	mathematical	ContinuousWithinAt	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsWithin Filter.comap Set.image	—	Filter.Tendsto.le_comap ContinuousWithinAt.tendsto_nhdsWithin_image

---

← Back to Index