Restrict

📁 Source: Mathlib/Data/Set/Restrict.lean

Statistics

Metric	Count
Definitions codRestrict, restrict, restrict₂	3
Theorems restrictPreimage, codRestrict, restrictPreimage, restrictPreimage, injective, coe_iterate_restrict, coe_restrict, range_restrict, restrict_commutes, restrict_eq_codRestrict, restrict_inj, restrict_surjective_iff, val_restrict_apply, codRestrict_range_surjective, codRestrict_restrict, eq_restrict_iff, image_restrict, image_restrictPreimage, image_val_preimage_restrictPreimage, injOn_iff_injective, injective_codRestrict, mapsTo_iff_exists_map_subtype, preimage_restrictPreimage, range_codRestrict, range_extend, range_extend_subset, range_restrict, range_restrictPreimage, restrictPreimage_bijective, restrictPreimage_injective, restrictPreimage_mk, restrictPreimage_surjective, restrict_apply, restrict_comp_codRestrict, restrict_def, restrict_dite, restrict_dite_compl, restrict_eq, restrict_eq_iff, restrict_eq_restrict_iff, restrict_extend_compl_range, restrict_extend_range, restrict_id, restrict_ite, restrict_ite_compl, restrict_piecewise, restrict_piecewise_compl, restrict₂_comp_restrict, restrict₂_comp_restrict₂, restrict₂_def, surjOn_iff_surjective, surjective_codRestrict, surjective_mapsTo_image_restrict, val_codRestrict_apply	54
Total	57

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	Function.Bijective	Set.Elem Set.preimage Set.restrictPreimage	—	Set.restrictPreimage_bijective

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	Set Set.instMembership	Set.Elem Set.codRestrict	—	Set.injective_codRestrict
restrictPreimage 📖	mathematical	—	Set.Elem Set.preimage Set.restrictPreimage	—	Set.restrictPreimage_injective

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	—	Set.Elem Set.preimage Set.restrictPreimage	—	Set.restrictPreimage_surjective

Set

Definitions

Name	Category	Theorems
codRestrict 📖	CompOp	23 math math: Orthonormal.codRestrict, Topology.IsInducing.codRestrict, IsOpenMap.codRestrict, IsCompactOperator.codRestrict, surjective_codRestrict, injective_codRestrict, Function.Injective.codRestrict, codRestrict_range_surjective, ContinuousAt.codRestrict, MapsTo.restrict_eq_codRestrict, restrict_comp_codRestrict, StrictMono.codRestrict, range_codRestrict, Monotone.codRestrict, continuousAt_codRestrict_iff, IsClosedMap.codRestrict, Continuous.codRestrict, codRestrict_restrict, Topology.IsEmbedding.codRestrict, ContMDiff.codRestrict_sphere, AntilipschitzWith.codRestrict, AEMeasurable.subtype_mk, val_codRestrict_apply
restrict 📖	CompOp	167 math math: cfcₙ_def, restrict_dite, UniformOnFun.gen_eq_preimage_restrict, ApproximatesLinearOn.lipschitz, OpenPartialHomeomorph.subtypeRestr_coe, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', MeasureTheory.measurable_restrict_cylinderEvents, image_coe_eq_restrict_image, AlgebraicIndependent.restrict_of_comp_subtype, surjOn_iff_surjective, restrict_apply, UniformOnFun.isometry_restrict, equicontinuous_restrict_iff, LinearIndepOn.linearIndependent_restrict, restrict_def, MapsTo.coe_restrict, cfc_apply_mkD, cfcₙ_eq_cfcₙL_mkD, AntilipschitzWith.to_rightInvOn, restrict_extend_range, uniformEquicontinuous_restrict_iff, cfcₙ_apply_mkD, Pi.induced_restrict, lipschitzOnWith_iff_restrict, Finset.piCongrLeft_comp_restrict, EquicontinuousOn.inducing_uniformOnFun_iff_pi', ContinuousMap.mkD_of_continuousOn, ContinuousMap.mkD_of_not_continuousOn, Pi.uniformSpace_comap_restrict, linearIndependent_restrict_iff, AddSubgroup.isComplement_addSubgroup_left_iff_bijective, HolderOnWith.holderWith, restrict_piecewise, semicontinuous_restrict_iff, isClosedMap_restrict_of_compactSpace, ContinuousMap.coe_restrict, isLocalHomeomorph_iff_isOpenEmbedding_restrict, uniformContinuousOn_iff_restrict, ConvexOn.sSup_of_countable_affine_eq, Topology.reorderRestrictProd_restrict_compl, MeasureTheory.measurableEmbedding_of_fderivWithin, ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, injOn_iff_injective, LocallyLipschitzOn.restrict, EquicontinuousOn.isClosed_range_pi_of_uniformOnFun', Topology.reorderRestrictProd_mem_preimage_image_restrict, dependsOn_restrict, cfc_def, InjOn.injective, MapsTo.restrict_eq_codRestrict, OpenPartialHomeomorph.isOpenEmbedding_restrict, UniformOnFun.continuous_rng_iff, Topology.reorderRestrictProd_of_mem, AddSubgroup.isComplement_addSubgroup_right_iff_bijective, ConvexOn.sSup_of_nat_affine_eq, restrict₂_comp_restrict, restrict_comp_codRestrict, UniformOnFun.topologicalSpace_eq, isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, range_restrict, ContinuousOn.measurableEmbedding, Topology.continuous_reorderRestrictProd, LinearMap.coe_domRestrict, Topology.image_snd_preimageImageRestrict, cfc_eq_cfcL_mkD, ApproximatesLinearOn.antilipschitz, lowerHemicontinuous_restrict_iff, ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry, restrict_ite_compl, restrict_dite_compl, EquicontinuousOn.comap_uniformOnFun_eq, LipschitzWith.restrict, IsOpenMap.restrict, ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun, OrdConnected.restrict, tendsto_nhdsWithin_iff_subtype, Finsupp.linearCombination_restrict, MeasureTheory.Filtration.piFinset_eq_comap_restrict, Pi.continuous_restrict, measurable_restrict_apply, HolderWith.restrict_iff, restrict_extend_compl_range, UniformOnFun.uniformContinuous_restrict, Function.Embedding.invFun_restrict, tendstoUniformlyOn_iff_restrict, Pi.induced_restrict_sUnion, cfc_apply, ContinuousMap.mkD_apply_of_continuousOn, UniformOnFun.edist_eq_pi_restrict, measurable_restrict, continuousOn_iff_continuous_restrict, restrict_ite, ConvexOn.real_sSup_of_countable_affine_eq, lowerSemicontinuous_restrict_iff, ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, UniformOnFun.uniformContinuous_restrict_toFun, AddCircle.liftIoc_eq_lift_Icc, Subgroup.isComplement_subgroup_left_iff_bijective, Pi.continuous_restrict_apply, piCongrLeft_comp_restrict, strictMono_restrict, ContinuousOn.restrict, cfc_apply_pi, StrictMonoOn.restrict, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar, UniformOnFun.edist_continuousRestrict, ContinuousMap.continuousOn_mkD_restrict_of_uncurry, IsCompact.isClosed_image_restrict, ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound, codRestrict_restrict, ContinuousMap.continuous_mkD_restrict_of_uncurry, restrict_eq, Finset.restrict_preimage, AntilipschitzWith.restrict, cfcₙ_apply_pi, ContinuousMapZero.mkD_of_not_continuousOn, ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound, restrict_eq_iff, LipschitzOnWith.to_restrict, Pi.uniformSpace_comap_restrict_sUnion, continuousWithinAt_iff_continuousAt_restrict, cfc_eq_cfcL, lipschitzOnWith_restrict, Monotone.restrict, equicontinuousAt_restrict_iff, ContinuousMapZero.aeStronglyMeasurable_mkD_restrict_of_uncurry, ApproximatesLinearOn.injective, IsClosedMap.restrict, cfcₙ_eq_cfcₙL, UniformOnFun.edist_eq_restrict_sUnion, image_image_val_eq_restrict_image, ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn, restrict_eq_restrict_iff, ContinuousMapZero.mkD_of_continuousOn, dependsOn_iff_exists_comp, UniformOnFun.edist_continuousRestrict_of_singleton, image_restrict, ContinuousMapZero.mkD_apply_of_continuousOn, UniformOnFun.isUniformInducing_pi_restrict, ConvexOn.exists_affine_le_of_lt, Pi.uniformContinuous_restrict, upperHemicontinuousOn_iff_restrict, ConvexOn.real_sSup_of_nat_affine_eq, UniformOnFun.hasBasis_uniformity_of_basis_aux₁, cfcₙ_apply, Function.Injective.invFun_restrict, Topology.reorderRestrictProd_of_compl, AddCircle.liftIco_eq_lift_Icc, upperSemicontinuousOn_iff_restrict, Subgroup.isComplement_subgroup_right_iff_bijective, ConvexOn.sSup_affine_eq, UniformOnFun.lipschitzWith_restrict, ConvexOn.real_sSup_affine_eq, UniformOnFun.hasBasis_uniformity_of_basis_aux₂, hasSum_singleton, Topology.restrict_compl_reorderRestrictProd, restrict_id, MeasureTheory.Measure.infinitePi_map_restrict', dependsOn_iff_factorsThrough, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi', locallyLipschitzOn_iff_restrict, eq_restrict_iff, ApproximatesLinearOn.continuous, hasProd_singleton, ProbabilityTheory.Kernel.traj_eq_prod, restrict_piecewise_compl, Measurable.measurable_comp_iff_restrict
restrict₂ 📖	CompOp	7 math math: restrict₂_def, restrict₂_comp_restrict₂, restrict₂_comp_restrict, measurable_restrict₂, measurable_restrict₂_apply, Pi.continuous_restrict₂_apply, Pi.continuous_restrict₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict_range_surjective 📖	mathematical	—	Elem range codRestrict mem_range_self	—	mem_range_self
codRestrict_restrict 📖	mathematical	Set instMembership	codRestrict Elem restrict MapsTo.restrict	—	—
eq_restrict_iff 📖	mathematical	—	restrict Set instMembership	—	—
image_restrict 📖	mathematical	—	image Elem restrict preimage Set instMembership instInter	—	restrict_eq image_comp image_preimage_eq_inter_range Subtype.range_coe
image_restrictPreimage 📖	mathematical	—	image Elem preimage restrictPreimage Set instMembership	—	mapsTo_preimage Function.Injective.image_injective Subtype.coe_injective image_comp MapsTo.restrict_commutes Subtype.image_preimage_coe image_preimage_inter
image_val_preimage_restrictPreimage 📖	mathematical	—	image Set instMembership preimage Elem restrictPreimage	—	ext
injOn_iff_injective 📖	mathematical	—	InjOn Elem restrict	—	—
injective_codRestrict 📖	mathematical	Set instMembership	Elem codRestrict	—	—
mapsTo_iff_exists_map_subtype 📖	mathematical	—	MapsTo Set instMembership	—	Subtype.coe_prop
preimage_restrictPreimage 📖	mathematical	—	preimage Elem restrictPreimage Set instMembership image	—	preimage_preimage image_val_preimage_restrictPreimage preimage_image_eq Subtype.val_injective
range_codRestrict 📖	mathematical	Set instMembership	range Elem codRestrict preimage	—	ext
range_extend 📖	mathematical	—	range Function.extend Set instUnion image Compl.compl instCompl	—	HasSubset.Subset.antisymm instAntisymmSubset range_extend_subset Function.Injective.extend_apply Function.extend_apply'
range_extend_subset 📖	mathematical	—	Set instHasSubset range Function.extend instUnion image Compl.compl instCompl	—	Function.extend_def mem_range_self mem_image_of_mem
range_restrict 📖	mathematical	—	range Elem restrict image	—	range_comp Subtype.range_coe
range_restrictPreimage 📖	mathematical	—	range Elem preimage restrictPreimage Set instMembership	—	—
restrictPreimage_bijective 📖	mathematical	Function.Bijective	Elem preimage restrictPreimage	—	restrictPreimage_injective restrictPreimage_surjective
restrictPreimage_injective 📖	mathematical	—	Elem preimage restrictPreimage	—	Subtype.coe_injective mapsTo_preimage
restrictPreimage_mk 📖	mathematical	Set instMembership preimage	restrictPreimage	—	—
restrictPreimage_surjective 📖	mathematical	—	Elem preimage restrictPreimage	—	—
restrict_apply 📖	mathematical	—	restrict Set instMembership	—	—
restrict_comp_codRestrict 📖	mathematical	Set instMembership	Elem restrict codRestrict	—	—
restrict_def 📖	mathematical	—	restrict Set instMembership	—	—
restrict_dite 📖	mathematical	—	restrict Set instMembership	—	—
restrict_dite_compl 📖	mathematical	—	restrict Compl.compl Set instCompl instMembership	—	—
restrict_eq 📖	mathematical	—	restrict Set instMembership	—	—
restrict_eq_iff 📖	mathematical	—	restrict Set instMembership	—	—
restrict_eq_restrict_iff 📖	mathematical	—	restrict EqOn	—	restrict_eq_iff
restrict_extend_compl_range 📖	mathematical	—	restrict Compl.compl Set instCompl range Function.extend instMembership	—	restrict_dite_compl
restrict_extend_range 📖	mathematical	—	restrict range Function.extend Set instMembership Subtype.coe_prop	—	restrict_dite
restrict_id 📖	mathematical	—	restrict Set instMembership	—	—
restrict_ite 📖	mathematical	—	restrict Set instMembership	—	restrict_dite
restrict_ite_compl 📖	mathematical	—	restrict Compl.compl Set instCompl instMembership	—	restrict_dite_compl
restrict_piecewise 📖	mathematical	—	restrict piecewise	—	restrict_ite
restrict_piecewise_compl 📖	mathematical	—	restrict Compl.compl Set instCompl piecewise	—	restrict_ite_compl
restrict₂_comp_restrict 📖	mathematical	Set instHasSubset	restrict₂ restrict	—	—
restrict₂_comp_restrict₂ 📖	mathematical	Set instHasSubset	restrict₂ HasSubset.Subset.trans instIsTransSubset	—	—
restrict₂_def 📖	mathematical	Set instHasSubset	restrict₂ instMembership	—	—
surjOn_iff_surjective 📖	mathematical	—	SurjOn univ Elem restrict	—	—
surjective_codRestrict 📖	mathematical	Set instMembership	Elem codRestrict range	—	range_codRestrict Subtype.range_coe_subtype Subset.antisymm_iff
surjective_mapsTo_image_restrict 📖	mathematical	—	Elem image MapsTo.restrict mapsTo_image	—	mapsTo_image
val_codRestrict_apply 📖	mathematical	Set instMembership	codRestrict	—	—

Set.InjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	mathematical	Set.InjOn	Set.Elem Set.restrict	—	Set.injOn_iff_injective

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_iterate_restrict 📖	mathematical	Set.MapsTo	Set Set.instMembership Nat.iterate Set.Elem restrict	—	Function.iterate_succ'
coe_restrict 📖	mathematical	Set.MapsTo	Set.Elem Set Set.instMembership restrict Set.restrict	—	—
range_restrict 📖	mathematical	Set.MapsTo	Set.range Set.Elem restrict Set.preimage Set Set.instMembership Set.image	—	Set.range_subtype_map
restrict_commutes 📖	mathematical	Set.MapsTo	Set.Elem Set Set.instMembership restrict	—	—
restrict_eq_codRestrict 📖	mathematical	Set.MapsTo	restrict Set.codRestrict Set.Elem Set.restrict Set Set.instMembership	—	—
restrict_inj 📖	mathematical	Set.MapsTo	Set.Elem restrict Set.InjOn	—	restrict_eq_codRestrict Set.injective_codRestrict Set.injOn_iff_injective
restrict_surjective_iff 📖	mathematical	Set.MapsTo	Set.Elem restrict Set.SurjOn	—	Set.mem_image_of_mem
val_restrict_apply 📖	mathematical	Set.MapsTo	Set Set.instMembership restrict	—	—

---

← Back to Index