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`, `restrict_mapsTo`, `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_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`	170
Total	171

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_continuousOn` 📖	—	`Continuous` `ContinuousOn`	—	—	`ContinuousOn.comp` `continuousOn` `Set.mapsTo_univ`
`comp_continuousOn'` 📖	—	`Continuous` `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.preimage`	—	`nhdsSetWithin_univ` `preimage_mem_nhdsSetWithin`
`preimage_mem_nhdsSetWithin` 📖	mathematical	`Continuous` `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` 📖	—	`ContinuousAt` `ContinuousWithinAt`	—	—	`ContinuousWithinAt.comp` `continuousWithinAt` `Set.mapsTo_univ`
`comp_continuousWithinAt_of_eq` 📖	—	`ContinuousAt` `ContinuousWithinAt`	—	—	`comp_continuousWithinAt`
`comp₂_continuousWithinAt` 📖	—	`ContinuousAt` `instTopologicalSpaceProd` `ContinuousWithinAt`	—	—	`comp_continuousWithinAt` `Filter.Tendsto.prodMk_nhds`
`comp₂_continuousWithinAt_of_eq` 📖	—	`ContinuousAt` `instTopologicalSpaceProd` `ContinuousWithinAt`	—	—	`comp₂_continuousWithinAt`
`congr_of_eventuallyEq` 📖	—	`ContinuousAt` `Filter.EventuallyEq` `nhds`	—	—	`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` 📖	—	`ContinuousOn` `Set.MapsTo`	—	—	`ContinuousWithinAt.comp`
`comp'` 📖	—	`ContinuousOn` `Set.MapsTo`	—	—	`comp`
`comp_continuous` 📖	—	`ContinuousOn` `Continuous` `Set` `Set.instMembership`	—	—	`continuousOn_univ` `comp`
`comp_inter` 📖	mathematical	`ContinuousOn`	`Set` `Set.instInter` `Set.preimage`	—	`comp` `mono` `Set.inter_subset_left` `Set.inter_subset_right`
`congr_mono` 📖	—	`ContinuousOn` `Set.EqOn` `Set` `Set.instHasSubset`	—	—	`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`	`Fin.cons`	—	`ContinuousWithinAt.finCons`
`finInsertNth` 📖	mathematical	`ContinuousOn` `Pi.topologicalSpace` `Fin.succAbove`	`Fin.insertNth`	—	`ContinuousWithinAt.finInsertNth`
`finSnoc` 📖	mathematical	`ContinuousOn` `Pi.topologicalSpace`	`Fin.snoc`	—	`ContinuousWithinAt.finSnoc`
`fst` 📖	—	`ContinuousOn` `instTopologicalSpaceProd`	—	—	`Continuous.comp_continuousOn` `continuous_fst`
`iUnion_of_isOpen` 📖	mathematical	`ContinuousOn` `IsOpen`	`Set.iUnion`	—	`ContinuousAt.continuousWithinAt` `continuousAt` `IsOpen.mem_nhds`
`image_closure` 📖	mathematical	`ContinuousOn` `closure`	`Set` `Set.instHasSubset` `Set.image`	—	`ContinuousWithinAt.image_closure` `ContinuousWithinAt.mono` `subset_closure`
`image_comp_continuous` 📖	—	`ContinuousOn` `Set.image` `Continuous`	—	—	`comp` `Continuous.continuousOn` `Set.mapsTo_image`
`isOpen_inter_preimage` 📖	mathematical	`ContinuousOn` `IsOpen`	`Set` `Set.instInter` `Set.preimage`	—	`continuousOn_open_iff`
`isOpen_preimage` 📖	—	`ContinuousOn` `IsOpen` `Set` `Set.instHasSubset` `Set.preimage`	—	—	`Set.inter_comm` `Set.inter_eq_self_of_subset_left` `continuousOn_open_iff`
`iterate` 📖	mathematical	`ContinuousOn` `Set.MapsTo`	`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`	`Matrix.vecCons`	—	`ContinuousWithinAt.matrixVecCons`
`mono` 📖	—	`ContinuousOn` `Set` `Set.instHasSubset`	—	—	`Filter.Tendsto.mono_left` `nhdsWithin_mono`
`mono_dom` 📖	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `ContinuousOn`	—	—	`Filter.map_mono` `inf_le_inf_right` `nhds_mono`
`mono_rng` 📖	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `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.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`	`nhdsSetWithin` `Set.instInter` `Set.preimage`	—	`nhdsSetWithin_univ` `Set.inter_univ` `preimage_mem_nhdsSetWithin`
`prodMap` 📖	mathematical	`ContinuousOn`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`ContinuousWithinAt.prodMap`
`prodMk` 📖	mathematical	`ContinuousOn`	`instTopologicalSpaceProd`	—	`ContinuousWithinAt.prodMk`
`restrict` 📖	mathematical	`ContinuousOn`	`Continuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	`continuousOn_iff_continuous_restrict`
`restrict_mapsTo` 📖	mathematical	`ContinuousOn` `Set.MapsTo`	`Continuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.MapsTo.restrict`	—	`mapsToRestrict`
`snd` 📖	—	`ContinuousOn` `instTopologicalSpaceProd`	—	—	`Continuous.comp_continuousOn` `continuous_snd`
`tendsto_nhdsSet` 📖	mathematical	`ContinuousOn` `Set` `Filter` `Filter.instMembership` `nhdsSet` `Set.MapsTo`	`Filter.Tendsto`	—	`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` 📖	—	`Set` `Set.instMembership` `ContinuousOn` `instTopologicalSpaceProd` `SProd.sprod` `Set.instSProd`	—	—	`congr` `comp` `Continuous.continuousOn` `Continuous.prodMk` `continuous_const` `continuous_id'`
`uncurry_right` 📖	—	`Set` `Set.instMembership` `ContinuousOn` `instTopologicalSpaceProd` `SProd.sprod` `Set.instSProd`	—	—	`congr` `comp` `Continuous.continuousOn` `Continuous.prodMk` `continuous_id'` `continuous_const`
`union_continuousAt` 📖	mathematical	`IsOpen` `ContinuousOn` `ContinuousAt`	`Set` `Set.instUnion`	—	`continuousOn_of_forall_continuousAt` `ContinuousWithinAt.continuousAt` `continuousWithinAt` `IsOpen.mem_nhds`
`union_of_isClosed` 📖	mathematical	`ContinuousOn`	`Set` `Set.instUnion`	—	`ContinuousWithinAt.union` `continuousWithinAt_of_notMem_closure` `IsClosed.closure_eq`
`union_of_isOpen` 📖	mathematical	`ContinuousOn` `IsOpen`	`Set` `Set.instUnion`	—	`union_continuousAt` `IsOpen.continuousOn_iff`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`ContinuousWithinAt` `Set.MapsTo`	—	—	`Filter.Tendsto.comp` `tendsto` `tendsto_nhdsWithin`
`comp_inter` 📖	mathematical	`ContinuousWithinAt`	`Set` `Set.instInter` `Set.preimage`	—	`comp` `mono` `Set.inter_subset_left` `Set.inter_subset_right`
`comp_inter_of_eq` 📖	mathematical	`ContinuousWithinAt`	`Set` `Set.instInter` `Set.preimage`	—	`comp_inter`
`comp_of_eq` 📖	—	`ContinuousWithinAt` `Set.MapsTo`	—	—	`comp`
`comp_of_mem_nhdsWithin_image` 📖	—	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.image`	—	—	`comp` `mono_of_mem_nhdsWithin` `Set.mapsTo_image`
`comp_of_mem_nhdsWithin_image_of_eq` 📖	—	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.image`	—	—	`comp_of_mem_nhdsWithin_image`
`comp_of_preimage_mem_nhdsWithin` 📖	—	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	—	—	`Filter.Tendsto.comp` `tendsto` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within`
`comp_of_preimage_mem_nhdsWithin_of_eq` 📖	—	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	—	—	`comp_of_preimage_mem_nhdsWithin`
`congr_mono` 📖	—	`ContinuousWithinAt` `Set.EqOn` `Set` `Set.instHasSubset`	—	—	`congr` `mono`
`congr_of_eventuallyEq` 📖	—	`ContinuousWithinAt` `Filter.EventuallyEq` `nhdsWithin`	—	—	`Filter.EventuallyEq.congr_continuousWithinAt`
`congr_of_eventuallyEq_insert` 📖	—	`ContinuousWithinAt` `Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instInsert`	—	—	`congr_of_eventuallyEq` `nhdsWithin_mono` `Set.subset_insert` `mem_of_mem_nhdsWithin` `Set.mem_insert`
`congr_of_eventuallyEq_of_mem` 📖	—	`ContinuousWithinAt` `Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instMembership`	—	—	`congr_of_eventuallyEq` `mem_of_mem_nhdsWithin`
`congr_of_insert` 📖	—	`ContinuousWithinAt`	—	—	`congr` `Set.mem_insert_of_mem` `Set.mem_insert`
`congr_of_mem` 📖	—	`ContinuousWithinAt` `Set` `Set.instMembership`	—	—	`congr`
`congr_set` 📖	—	`ContinuousWithinAt` `Filter.EventuallyEq` `nhds`	—	—	`continuousWithinAt_congr_set`
`continuousAt` 📖	mathematical	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`ContinuousAt`	—	`continuousWithinAt_iff_continuousAt`
`diff_iff` 📖	mathematical	`ContinuousWithinAt`	`Set` `Set.instSDiff`	—	`mono` `union` `Set.diff_union_self` `Set.diff_subset`
`finCons` 📖	mathematical	`ContinuousWithinAt` `Pi.topologicalSpace`	`Fin.cons`	—	`Filter.Tendsto.finCons` `tendsto`
`finInsertNth` 📖	mathematical	`ContinuousWithinAt` `Pi.topologicalSpace` `Fin.succAbove`	`Fin.insertNth`	—	`Filter.Tendsto.finInsertNth` `tendsto`
`finSnoc` 📖	mathematical	`ContinuousWithinAt` `Pi.topologicalSpace`	`Fin.snoc`	—	`Filter.Tendsto.finSnoc` `tendsto`
`fst` 📖	—	`ContinuousWithinAt` `instTopologicalSpaceProd`	—	—	`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`	`Set` `Set.instInsert`	—	`continuousWithinAt_insert_self`
`matrixVecCons` 📖	mathematical	`ContinuousWithinAt` `Pi.topologicalSpace`	`Matrix.vecCons`	—	`Filter.Tendsto.matrixVecCons` `tendsto`
`mem_closure` 📖	—	`ContinuousWithinAt` `Set` `Set.instMembership` `closure` `Set.MapsTo`	—	—	`closure_mono` `Set.image_subset_iff` `mem_closure_image`
`mem_closure_image` 📖	mathematical	`ContinuousWithinAt` `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` 📖	—	`ContinuousWithinAt` `Set` `Set.instHasSubset`	—	—	`Filter.Tendsto.mono_left` `nhdsWithin_mono`
`mono_of_mem_nhdsWithin` 📖	—	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`Filter.Tendsto.mono_left` `nhdsWithin_le_of_mem`
`preimage_mem_nhdsWithin` 📖	mathematical	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin` `Set.preimage`	—	—
`preimage_mem_nhdsWithin'` 📖	mathematical	`ContinuousWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.image`	`Set.preimage`	—	`tendsto_nhdsWithin` `Set.mapsTo_image`
`preimage_mem_nhdsWithin''` 📖	—	`ContinuousWithinAt` `Set.preimage` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`preimage_mem_nhdsWithin'` `nhdsWithin_mono` `Set.image_preimage_subset`
`prodMap` 📖	mathematical	`ContinuousWithinAt`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`prodMk` `comp` `continuousWithinAt_fst` `Set.mapsTo_fst_prod` `continuousWithinAt_snd` `Set.mapsTo_snd_prod`
`prodMk` 📖	mathematical	`ContinuousWithinAt`	`instTopologicalSpaceProd`	—	`Filter.Tendsto.prodMk_nhds`
`snd` 📖	—	`ContinuousWithinAt` `instTopologicalSpaceProd`	—	—	`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`	`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`	—	`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`	—	`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` 📖	—	`Set.MapsTo` `ContinuousOn` `closure`	—	—	`closure_of_continuousWithinAt` `ContinuousWithinAt.mono` `subset_closure`
`closure_of_continuousWithinAt` 📖	mathematical	`Set.MapsTo` `ContinuousWithinAt`	`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	265 math math: `continuousOn_ceil`, `cfcₙ_def`, `Real.continuousOn_rpowIntegrand₀₁_uncurry`, `AnalyticOn.continuousOn`, `continuousOn_stereoToFun`, `Complex.continuousOn_exp`, `intervalIntegral.continuousOn_primitive_interval`, `ConvexOn.continuousOn_tfae`, `Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure`, `Set.Subsingleton.continuousOn`, `ApproximatesLinearOn.inverse_continuousOn`, `WithTop.continuousOn_untopD`, `mdifferentiableOn_iff`, `continuousOn_boolIndicator_iff_isClopen`, `ChartedSpaceCore.continuousOn_toFun`, `continuousOn_prod_of_discrete_right`, `antitone_continuousOn`, `DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv`, `Uniform.continuousOn_iff'_left`, `continuousOn_dslope`, `continuousOn_floor`, `HasGradientAt.continuousOn`, `Topology.RelCWComplex.continuousOn_symm`, `Topology.CWComplex.continuousOn`, `Complex.continuousOn_arg`, `Unitary.continuousOn_argSelfAdjoint`, `OpenPartialHomeomorph.continuousOn_univBall_symm`, `continuousOn_neg`, `Continuous.continuousOn`, `ContinuousAlgEquiv.continuousOn`, `contDiffOn_iff_continuousOn_differentiableOn`, `FiberPrebundle.continuous_trivChange`, `IsOpenMap.continuousOn_range_of_leftInverse`, `IsOpen.continuousOn_iff`, `DifferentiableOn.continuousOn`, `FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas`, `intervalIntegral.continuousOn_primitive`, `continuousOn_fract`, `HasDerivAt.continuousOn`, `contDiffOn_nat_iff_continuousOn_differentiableOn_deriv`, `Complex.continuousOn_cos`, `continuousOn_of_forall_continuousAt`, `continuousOn_star`, `intervalIntegral.continuousOn_primitive_interval_left`, `continuousOn_iUnion_iff_of_isOpen`, `CFC.continuousOn_log`, `Topology.RelCWComplex.continuousOn`, `Real.continuousOn_log`, `Trivialization.Prod.continuous_inv_fun`, `LipschitzOnWith.continuousOn`, `Trivialization.continuousOn`, `continuousOn_zpow`, `continuousOn_congr`, `ENNReal.continuousOn_sub`, `CFC.continuousOn_sqrt`, `ODE.FunSpace.continuousOn_comp_compProj`, `Topology.IsCoherentWith.continuous_iff`, `ContDiffOn.continuousOn_iteratedDerivWithin`, `continuousOn_iff`, `continuousOn_singleton`, `ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux'`, `contDiffAt_one_iff`, `MDifferentiableOn.continuousOn`, `continuousOn_tangentCoordChange`, `mdifferentiableOn_iff_target`, `lipschitzOnWith_cfc_fun_of_subset`, `continuousOn_cfc_setProd`, `IsometryEquiv.comp_continuousOn_iff`, `AffineIsometryEquiv.continuousOn`, `ContDiffOn.continuousOn_iteratedFDerivWithin`, `contDiffWithinAt_zero`, `HasFTaylorSeriesUpToOn.cont`, `IsPicardLindelof.continuousOn`, `continouousOn_union_iff_of_isClosed`, `contDiffOn_nat_iff_continuousOn_differentiableOn`, `Complex.continuousOn_sin`, `HurwitzZeta.continuousOn_cosKernel`, `continuousOn_zsmul`, `continuousOn_const`, `ConcaveOn.continuousOn`, `intervalIntegral.continuousOn_primitive_Icc`, `ContDiffOn.continuousOn_zero`, `hasFTaylorSeriesUpToOn_zero_iff`, `Polynomial.continuousOn`, `Complex.continuousOn_norm_circleTransformBoundingFunction`, `continuousOn_pow`, `continuousOn_extChartAt`, `SeparationQuotient.continuousOn_lift`, `Units.continuousOn_zpow₀_spectrum`, `ZetaAsymptotics.continuousOn_term`, `continuousOn_inv`, `Set.EquicontinuousOn.continuousOn_of_mem`, `continuousOn_extendFrom`, `Real.continuousOn_cos`, `cfc_def`, `HasFPowerSeriesWithinOnBall.continuousOn`, `ContMDiffOn.continuousOn_tangentMapWithin`, `Uniform.continuousOn_iff'_right`, `equicontinuousOn_iff_continuousOn`, `DiffContOnCl.continuousOn_ball`, `IsLocalHomeomorphOn.continuousOn`, `HurwitzZeta.continuousOn_evenKernel`, `OpenPartialHomeomorph.continuousOn_extend_symm`, `Real.continuousOn_logb`, `lipschitzOnWith_cfc_fun`, `Filter.Tendsto.continuousOn_of_equicontinuousOn`, `IsPicardLindelof.continuousOn_uncurry`, `continuousOn_div`, `ENNReal.continuousOn_sub_left`, `continuousOn_inv₀`, `contDiffOn_zero`, `HurwitzZeta.continuousOn_oddKernel`, `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_apply`, `CFC.continuousOn_nnrpow`, `continuousOn_update_iff`, `ContinuousOn.continuousOn_iteratedFDerivWithin`, `UniformContinuousOn.continuousOn`, `ContMDiffOn.continuousOn`, `lipschitzOnWith_cfcₙ_fun`, `ContinuousLinearEquiv.comp_continuousOn_iff`, `Real.continuousOn_exp`, `continuousOn_const_smul_iff₀`, `continuousOn_isOpen_of_generateFrom`, `ContDiffOn.continuousOn_fderivWithin_apply`, `Topology.IsEmbedding.continuousOn_iff`, `Dilation.comp_continuousOn_iff`, `OpenPartialHomeomorph.continuousOn_invFun`, `Homeomorph.comp_continuousOn_iff`, `Complex.continuousOn_tan`, `UniformOnFun.continuousOn_eval₂`, `ContDiffOn.continuousOn_derivWithin`, `Real.continuousOn_sin`, `continuousOn_snd`, `ContDiffOn.continuousOn_fderivWithin`, `AnalyticOnNhd.continuousOn`, `HasFiniteFPowerSeriesOnBall.continuousOn`, `Set.Finite.continuousOn`, `continuousOn_fst`, `NNReal.continuousOn_rpow_const`, `VectorPrebundle.exists_coordChange`, `ConvexOn.locallyLipschitzOn_iff_continuousOn`, `continuousOn_inv_iff`, `Complex.continuousOn_prod_circle_transform_function`, `ModelWithCorners.continuousOn_symm`, `Real.continuousOn_rpowIntegrand₀₁_Ici`, `ContDiffOn.continuousOn_fderiv_of_isOpen`, `IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn`, `contMDiffOn_iff`, `ConcaveOn.continuousOn_interior`, `ENNReal.continuousOn_toNNReal`, `CPolynomialOn.continuousOn`, `continuousOn_extChartAt_symm`, `Trivialization.Prod.continuous_to_fun`, `continuousOn_const_smul_iff`, `Isometry.comp_continuousOn_iff`, `Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn`, `ContinuousLinearMap.continuousOn_uncurry_of_multilinear`, `OpenPartialHomeomorph.continuousOn`, `DiffContOnCl.continuousOn`, `lipschitzOnWith_cfcₙ_fun_of_subset`, `continuousOn_empty`, `continuousOn_iff_continuous_restrict`, `ZetaAsymptotics.continuousOn_term_tsum`, `contMDiffOn_iff_of_mem_maximalAtlas`, `Units.continuousOn_inv₀_spectrum`, `IsUnit.continuousOn_const_smul_iff`, `continuousOn_nsmul`, `VectorBundleCore.continuousOn_coordChange`, `LinearIsometryEquiv.continuousOn`, `Trivialization.continuousOn_proj`, `hasFTaylorSeriesUpToOn_succ_iff_left`, `ContDiffOn.continuousOn`, `ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux`, `contMDiffOn_iff_of_subset_source`, `Pretrivialization.continuousOn_continuousLinearMapCoordChange`, `continuousOn_prod_of_discrete_left`, `equicontinuousOn_unique`, `continuousOn_iff_isClosed`, `LinearIsometryEquiv.comp_continuousOn_iff`, `VectorPrebundle.continuousOn_coordChange`, `upperHemicontinuousOn_singleton_iff`, `Real.continuousOn_tan`, `contDiffAt_zero`, `continuousOn_cfcₙ_setProd`, `continuousOn_toIocDiv`, `OpenPartialHomeomorph.continuousOn_toFun`, `NormedSpace.continuousOn_exp`, `ConvexOn.continuousOn_interior`, `NNReal.continuousOn_rpow_const_compl_zero`, `continuousOn_id'`, `HasFPowerSeriesOnBall.continuousOn`, `ConcaveOn.continuousOn_tfae`, `IsMIntegralCurveOn.continuousOn`, `OpenPartialHomeomorph.continuousOn_symm`, `ApproximatesLinearOn.continuousOn`, `continuousOn_open_iff`, `FiberBundleCore.continuousOn_coordChange`, `continuousOn_toIcoDiv`, `AffineIsometryEquiv.comp_continuousOn_iff`, `HasDerivWithinAt.continuousOn`, `ENNReal.continuousOn_toReal`, `ContDiffOn.continuousOn_deriv_of_isOpen`, `continuousOn_iff'`, `SeparationQuotient.continuousOn_lift₂`, `Topology.IsInducing.continuousOn_iff`, `Metric.continuousOn_iff'`, `continuousOn_cfc_nnreal_setProd`, `IsOpenMap.continuousOn_image_of_leftInvOn`, `intervalIntegral.continuousOn_primitive_interval'`, `continuousOn_id`, `continuousOn_univ`, `ContinuousOn.continuousOn_iteratedFDeriv`, `WithTop.continuousOn_untopA`, `OpenPartialHomeomorph.continuousOn_extend`, `continuousOn_taylorWithinEval`, `continuousOn_zpow₀`, `Real.continuousOn_rpowIntegrand₀₁`, `Metric.continuousOn_iff`, `Real.continuousOn_arcosh`, `continuousOn_to_generateFrom_iff`, `contMDiffOn_iff_target`, `Topology.IsInducing.continuousOn_image_iff`, `continuousOn_of_locally_uniform_approx_of_continuousWithinAt`, `contDiffOn_iff_continuousOn_differentiableOn_deriv`, `contMDiffOn_zero_iff`, `Topology.CWComplex.continuousOn_symm`, `Trivialization.continuousOn_symm`, `continuousOn_cfcₙ_nnreal_setProd`, `ContinuousLinearEquiv.continuousOn`, `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_neg_iff`, `continuousOn_pi`, `Polynomial.continuousOn_aeval`, `ContinuousSqrt.continuousOn_sqrt`, `mdifferentiableOn_iff_of_mem_maximalAtlas`, `OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left`, `continuousOn_coordChange`, `IsCoveringMapOn.continuousOn`, `DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁`, `ConcaveOn.locallyLipschitzOn_iff_continuousOn`, `LocallyFinite.continuousOn_iUnion'`, `ConvexOn.continuousOn`, `Complex.continuousOn_one_add_mul_inv`, `continuousOn_const_vadd_iff`, `equicontinuousOn_finite`, `Real.continuousOn_tan_Ioo`, `continouousOn_union_iff_of_isOpen`, `unitary.continuousOn_argSelfAdjoint`

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.mono` `Set.subset_union_left` `Set.subset_union_right` `ContinuousOn.union_of_isClosed`
`continouousOn_union_iff_of_isOpen` 📖	mathematical	`IsOpen`	`ContinuousOn` `Set` `Set.instUnion`	—	`ContinuousOn.mono` `Set.subset_union_left` `Set.subset_union_right` `ContinuousOn.union_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` `IsOpen` `Set` `Set.instMembership` `Set.instHasSubset` `Set.instInter` `Set.preimage`	—	—
`continuousOn_iff'` 📖	mathematical	—	`ContinuousOn` `IsOpen` `Set` `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` `IsClosed` `Set` `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` 📖	—	`IsOpen` `Set` `Set.instMembership` `ContinuousOn` `Set.instInter`	—	—	`nhdsWithin_restrict` `ContinuousWithinAt.eq_1`
`continuousOn_open_iff` 📖	mathematical	`IsOpen`	`ContinuousOn` `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`	`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`	—	`forall_swap`
`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` `forall_swap`
`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.restrict`	—	`tendsto_nhdsWithin_iff_subtype`
`continuousWithinAt_insert_self` 📖	mathematical	—	`ContinuousWithinAt` `Set` `Set.instInsert`	—	—
`continuousWithinAt_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`ContinuousWithinAt` `Set.instInter`	—	`nhdsWithin_restrict'`
`continuousWithinAt_inter'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`ContinuousWithinAt` `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`	—	`forall_swap` `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