congr

📁 Source: MathlibTest/congr.lean

Statistics

Metric	Count
Definitions congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr	38
Theorems congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr, congr	154
Total	192

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	AEMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.trans Filter.EventuallyEq.symm

AddAut

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_apply, congr_symm_apply

AddCommGroup.DirectLimit

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_apply_of, congr_symm_apply_of

AddCon

Definitions

Name	Category	Theorems
congr 📖	CompOp	1 math math: congr_mk

AdicCompletion

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_symm_apply, congr_apply

Algebra.TensorProduct

Definitions

Name	Category	Theorems
congr 📖	CompOp	7 math math: congr_trans, congr_symm_apply, IsAzumaya.mulLeftRight_comp_congr, congr_toLinearEquiv, congr_apply, congr_refl, congr_symm

AlgebraicGeometry.PresheafedSpace.stalkMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.PresheafedSpace.Hom.stalkMap CategoryTheory.eqToHom	—	TopCat.Presheaf.stalk_hom_ext CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	AnalyticAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AnalyticAt	—	HasFPowerSeriesAt.analyticAt HasFPowerSeriesAt.congr

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	AnalyticOn Set.EqOn	AnalyticOn	—	AnalyticWithinAt.congr

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AnalyticOnNhd Set.EqOn	AnalyticOnNhd	—	congr' mem_nhdsSet_iff_forall Filter.eventuallyEq_iff_exists_mem IsOpen.mem_nhds

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	AnalyticWithinAt Set.EqOn	AnalyticWithinAt	—	congr_of_eventuallyEq Set.EqOn.eventuallyEq_nhdsWithin

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	AntitoneOn Set.EqOn	AntitoneOn	—	MonotoneOn.congr dual_right

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Asymptotics.IsBigO	Asymptotics.IsBigO	—	congr' Filter.univ_mem'

Asymptotics.IsBigOTVS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Asymptotics.IsBigOTVS ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddGroup.toContinuousENorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Asymptotics.IsBigOTVS ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddGroup.toContinuousENorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	congr' Filter.univ_mem'

Asymptotics.IsBigOWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Asymptotics.IsBigOWith	Asymptotics.IsBigOWith	—	congr' Filter.univ_mem'

Asymptotics.IsLittleO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Asymptotics.IsLittleO	Asymptotics.IsLittleO	—	congr' Filter.univ_mem'

Asymptotics.IsLittleOTVS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Asymptotics.IsLittleOTVS ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddGroup.toContinuousENorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Asymptotics.IsLittleOTVS ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddGroup.toContinuousENorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	congr' Filter.univ_mem'

Asymptotics.SuperpolynomialDecay

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay	—	Filter.Tendsto.congr

BaireMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	BaireMeasurableSet Filter.EventuallyEq residual	BaireMeasurableSet	—	EventuallyMeasurableSet.congr countableInterFilter_residual Filter.EventuallyEq.symm

CPolynomialAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	CPolynomialAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	CPolynomialAt	—	HasFiniteFPowerSeriesAt.cpolynomialAt HasFiniteFPowerSeriesAt.congr

CPolynomialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup CPolynomialOn Set.EqOn	CPolynomialOn	—	congr' mem_nhdsSet_iff_forall Filter.eventuallyEq_iff_exists_mem IsOpen.mem_nhds

CategoryTheory.Grothendieck

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	Hom.fiber CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map Hom.base fiber CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp

CategoryTheory.Limits.cokernel

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_inv, congr_hom

CategoryTheory.Limits.kernel

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_inv, congr_hom

CategoryTheory.MonoOver

Definitions

Name	Category	Theorems
congr 📖	CompOp	4 math math: congr_unitIso, congr_functor, congr_inverse, congr_counitIso

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	app CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.eqToHom	—	naturality_assoc CategoryTheory.eqToHom_map CategoryTheory.eqToHom_trans CategoryTheory.Category.comp_id

CategoryTheory.Pseudofunctor.CoGrothendieck.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	fiber CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Pseudofunctor.CoGrothendieck.base CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.CoGrothendieck.fiber CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op base CategoryTheory.eqToHom CategoryTheory.Pseudofunctor.CoGrothendieck CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct	—	CategoryTheory.eqToHom_naturality CategoryTheory.Category.id_comp

CategoryTheory.Pseudofunctor.Grothendieck.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	fiber CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor.Grothendieck.base CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc base CategoryTheory.Pseudofunctor.Grothendieck.fiber CategoryTheory.eqToHom CategoryTheory.Pseudofunctor.Grothendieck CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct	—	CategoryTheory.Category.id_comp

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	CharP	—	—

CharacterModule

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

Con

Definitions

Name	Category	Theorems
congr 📖	CompOp	1 math math: congr_mk

ConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ConcaveOn Set.EqOn	ConcaveOn	—	—

ConformalAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Set Set.instMembership IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ConformalAt	ConformalAt	—	HasFDerivAt.congr_of_eventuallyEq Filter.Eventually.mono IsOpen.eventually_mem

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContDiffOn	ContDiffOn	—	ContDiffWithinAt.congr

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContDiffWithinAt	ContDiffWithinAt	—	congr_of_eventuallyEq Filter.eventuallyEq_of_mem self_mem_nhdsWithin

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContMDiff	ContMDiff	—	contMDiffOn_univ contMDiffOn_congr

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContMDiffOn	ContMDiffOn	—	StructureGroupoid.LocalInvariantProp.liftPropOn_congr contDiffWithinAt_localInvariantProp

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr contDiffWithinAt_localInvariantProp

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Continuous	Continuous	—	continuous_congr

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContinuousAt Filter.EventuallyEq nhds	ContinuousAt	—	continuousAt_congr

ContinuousLinearMap.HasLeftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContinuousLinearMap.HasLeftInverse	ContinuousLinearMap.HasLeftInverse	—	—

ContinuousLinearMap.HasRightInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContinuousLinearMap.HasRightInverse	ContinuousLinearMap.HasRightInverse	—	—

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContinuousOn Set.EqOn	ContinuousOn	—	congr_mono Set.Subset.refl

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ContinuousWithinAt	ContinuousWithinAt	—	congr_of_eventuallyEq Filter.mem_of_superset self_mem_nhdsWithin

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ConvexOn Set.EqOn	ConvexOn	—	—

Cycle.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	Cycle.Subsingleton Cycle Cycle.instMembership	—	—	instIsEmptyFalse

DFunLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	coe	—	—

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	DifferentiableOn	DifferentiableOn	—	DifferentiableWithinAt.congr

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	DifferentiableWithinAt	DifferentiableWithinAt	—	congr_mono Set.Subset.refl

Equiv.Set

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_symm_apply, congr_apply

EventuallyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	EventuallyMeasurable Filter.EventuallyEq	EventuallyMeasurable	—	EventuallyMeasurableSet.congr Filter.EventuallyEq.preimage

EventuallyMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	EventuallyMeasurableSet Filter.EventuallyEq	EventuallyMeasurableSet	—	Filter.EventuallyEq.trans

ExpChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	ExpChar	—	—

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.Eventually	Filter.Eventually	—	mp mono

Filter.EventuallyConst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyConst Filter.EventuallyEq	Filter.EventuallyConst	—	Filter.EventuallyEq.eventuallyConst_iff

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyLE Filter.EventuallyEq	Filter.EventuallyLE	—	Filter.Eventually.mp Filter.Eventually.mono

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.HasBasis	Filter.HasBasis	—	mem_iff

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.Tendsto	Filter.Tendsto	—	Filter.tendsto_congr

Finsupp

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

FormalMultilinearSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike	—	—

Function.Embedding

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_apply, Equiv.embeddingCongr_apply

GenLoop

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	HasDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul congr_mono Set.Subset.refl

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFDerivWithinAt Set.EqOn	HasFDerivWithinAt	—	congr_of_eventuallyEq Set.EqOn.eventuallyEq_nhdsWithin

HasFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFPowerSeriesAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	HasFPowerSeriesAt	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul EMetric.mem_nhds_iff HasFPowerSeriesOnBall.congr HasFPowerSeriesOnBall.mono lt_min HasFPowerSeriesOnBall.r_pos inf_le_left Metric.eball_subset_eball inf_le_right

HasFPowerSeriesOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFPowerSeriesOnBall Set.EqOn Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	HasFPowerSeriesOnBall	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul r_le r_pos Set.EqOn.symm edist_eq_enorm_sub add_sub_cancel_left sub_zero hasSum

HasFPowerSeriesWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFPowerSeriesWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	HasFPowerSeriesWithinAt	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul EMetric.mem_nhdsWithin_iff HasFPowerSeriesWithinOnBall.of_le HasFPowerSeriesWithinOnBall.r_pos min_le_left HasFPowerSeriesWithinOnBall.congr Metric.eball_subset_eball min_le_right

HasFPowerSeriesWithinOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFPowerSeriesWithinOnBall Set.EqOn Set Set.instInter Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	HasFPowerSeriesWithinOnBall	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul r_le r_pos AddLeftCancelSemigroup.toIsLeftCancelAdd add_zero edist_eq_enorm_sub add_sub_cancel_left sub_zero hasSum

HasFTaylorSeriesUpToOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFTaylorSeriesUpToOn	HasFTaylorSeriesUpToOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul zero_eq fderivWithin cont

HasFiniteFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFiniteFPowerSeriesAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	HasFiniteFPowerSeriesAt	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul finite HasFPowerSeriesAt.congr hasFPowerSeriesAt

HasFiniteFPowerSeriesOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasFiniteFPowerSeriesOnBall Set.EqOn Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	HasFiniteFPowerSeriesOnBall	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesOnBall.congr toHasFPowerSeriesOnBall finite

HasGradientWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasGradientWithinAt	HasGradientWithinAt	—	congr_mono

HasLineDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasLineDerivWithinAt Set.EqOn	HasLineDerivWithinAt	—	congr_mono Set.Subset.refl

HasProdUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasProdUniformly Filter.Eventually Finset Filter.atTop PartialOrder.toPreorder Finset.partialOrder	HasProdUniformly	—	hasProdUniformly_iff_tendstoUniformly tendstoUniformly_congr

HasProdUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasProdUniformlyOn Filter.Eventually Finset Set.EqOn Finset.prod Filter.atTop PartialOrder.toPreorder Finset.partialOrder	HasProdUniformlyOn	—	hasProdUniformlyOn_iff_tendstoUniformlyOn TendstoUniformlyOn.congr tendstoUniformlyOn

HasSumUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasSumUniformly Filter.Eventually Finset Filter.atTop PartialOrder.toPreorder Finset.partialOrder	HasSumUniformly	—	hasSumUniformly_iff_tendstoUniformly tendstoUniformly_congr

HasSumUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	HasSumUniformlyOn Filter.Eventually Finset Set.EqOn Finset.sum Filter.atTop PartialOrder.toPreorder Finset.partialOrder	HasSumUniformlyOn	—	hasSumUniformlyOn_iff_tendstoUniformlyOn TendstoUniformlyOn.congr tendstoUniformlyOn

IntervalIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Set.EqOn Real Set.uIoc Real.linearOrder IntervalIntegrable	IntervalIntegrable	—	intervalIntegrable_congr

Invertible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	invOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	invertible_unique

IsExtrFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsExtrFilter Filter.EventuallyEq	IsExtrFilter	—	eq_1 Filter.EventuallyEq.isMaxFilter_iff Filter.EventuallyEq.isMinFilter_iff

IsLocalExtr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsLocalExtr Filter.EventuallyEq nhds	IsLocalExtr	—	IsExtrFilter.congr Filter.EventuallyEq.eq_of_nhds

IsLocalExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsLocalExtrOn Filter.EventuallyEq nhdsWithin Set Set.instMembership	IsLocalExtrOn	—	IsExtrFilter.congr Filter.EventuallyEq.eq_of_nhdsWithin

IsLocalFrameOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsLocalFrameOn	IsLocalFrameOn	—	linearIndependent generating instReflLe ContMDiffOn.congr contMDiffOn

IsLocalMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsLocalMax Filter.EventuallyEq nhds	IsLocalMax	—	IsMaxFilter.congr Filter.EventuallyEq.eq_of_nhds

IsLocalMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsLocalMaxOn Filter.EventuallyEq nhdsWithin Set Set.instMembership	IsLocalMaxOn	—	IsMaxFilter.congr Filter.EventuallyEq.eq_of_nhdsWithin

IsLocalMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsLocalMin Filter.EventuallyEq nhds	IsLocalMin	—	IsMinFilter.congr Filter.EventuallyEq.eq_of_nhds

IsLocalMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsLocalMinOn Filter.EventuallyEq nhdsWithin Set Set.instMembership	IsLocalMinOn	—	IsMinFilter.congr Filter.EventuallyEq.eq_of_nhdsWithin

IsMaxFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsMaxFilter Filter.EventuallyEq	IsMaxFilter	—	Filter.EventuallyLE.isMaxFilter Filter.EventuallyEq.le Filter.EventuallyEq.symm

IsMinFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsMinFilter Filter.EventuallyEq	IsMinFilter	—	Filter.EventuallyLE.isMinFilter Filter.EventuallyEq.le

IsMulFreimanHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsMulFreimanHom Set.EqOn	IsMulFreimanHom	—	Set.MapsTo.congr mapsTo Multiset.map_congr map_prod_eq_map_prod

IsMulFreimanIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsMulFreimanIso Set.EqOn	IsMulFreimanIso	—	Set.BijOn.congr bijOn Multiset.map_congr Set.EqOn.symm map_prod_eq_map_prod

IsSemisimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	IsSemisimpleModule	—	RingHomInvPair.ids OrderIso.complementedLattice toComplementedLattice RingHomSurjective.ids

IsSimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	IsSimpleModule	—	RingHomInvPair.ids OrderIso.isSimpleOrder toIsSimpleOrder RingHomSurjective.ids

LineDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	LineDifferentiableWithinAt	LineDifferentiableWithinAt	—	congr_mono Set.Subset.refl

LinearIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	LinearIndepOn Set.EqOn	LinearIndepOn	—	linearIndepOn_congr

LinearMap.BilinForm

Definitions

Name	Category	Theorems
congr 📖	CompOp	9 math math: congr_apply, congr_comp, Nondegenerate.congr, congr_refl, congr_congr, nondegenerate_congr_iff, comp_congr, congr_trans, congr_symm

LinearMap.BilinForm.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	LinearMap.BilinForm.Nondegenerate	LinearMap.BilinForm.Nondegenerate DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.BilinForm LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.BilinForm.congr	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.SeparatingLeft.congr

LinearMap.IsPerfPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	LinearMap.compl₁₂ CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv.symm	LinearMap.IsPerfPair	—	Algebra.to_smulCommClass RingHomInvPair.ids compl₁₂ LinearMap.ext LinearEquiv.symm_apply_apply

LinearMap.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	LinearMap.Nondegenerate RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.Nondegenerate RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.arrowCongr RingHomCompTriple.ids LinearEquiv.refl	—	smulCommClass_self RingHomInvPair.ids RingHomCompTriple.ids LinearMap.SeparatingLeft.congr LinearMap.SeparatingRight.congr

LinearMap.SeparatingLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	LinearMap.SeparatingLeft RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.SeparatingLeft RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.arrowCongr RingHomCompTriple.ids LinearEquiv.refl	—	smulCommClass_self RingHomInvPair.ids RingHomCompTriple.ids LinearEquiv.map_eq_zero_iff LinearEquiv.symm_apply_apply

LinearMap.SeparatingRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	LinearMap.SeparatingRight RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.SeparatingRight RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.arrowCongr RingHomCompTriple.ids LinearEquiv.refl	—	smulCommClass_self RingHomInvPair.ids LinearMap.SeparatingLeft.congr

LinearMap.transvection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearMap.transvection LinearEquiv.symm NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule DFunLike.coe LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	—	RingHomInvPair.ids LinearMap.ext RingHomCompTriple.ids map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.apply_symm_apply map_smul SemilinearMapClass.toMulActionSemiHomClass

List.Vector

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MDifferentiableOn	MDifferentiableOn	—	StructureGroupoid.LocalInvariantProp.liftPropOn_congr differentiableWithinAt_localInvariantProp

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MDifferentiableWithinAt	MDifferentiableWithinAt	—	HasMFDerivWithinAt.mdifferentiableWithinAt HasMFDerivWithinAt.congr_mono hasMFDerivWithinAt Set.Subset.refl

Manifold.IsImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Manifold.IsImmersion	Manifold.IsImmersion	—	—

Manifold.IsImmersionOfComplement

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Manifold.IsImmersionOfComplement	Manifold.IsImmersionOfComplement	—	—

Manifold.IsLocalSourceTargetProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	Manifold.IsLocalSourceTargetProperty Set.EqOn PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	—	—

Mathlib.Tactic.FieldSimp.Sign

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasurableSet	MeasurableSet	—	—

MeasureTheory.AEDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.AEDisjoint Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEDisjoint	—	MeasureTheory.Measure.instOuterMeasureClass mono_ae Filter.EventuallyEq.le

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.AEStronglyMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.trans Filter.EventuallyEq.symm

MeasureTheory.HasFiniteIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.HasFiniteIntegral Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.HasFiniteIntegral	—	MeasureTheory.Measure.instOuterMeasureClass congr'_enorm Filter.EventuallyEq.fun_comp

MeasureTheory.HasPDF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.HasPDF	—	MeasureTheory.Measure.instOuterMeasureClass AEMeasurable.congr aemeasurable haveLebesgueDecomposition MeasureTheory.Measure.map_congr absolutelyContinuous

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.Integrable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Integrable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEStronglyMeasurable.congr MeasureTheory.HasFiniteIntegral.congr

MeasureTheory.IntegrableAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.IntegrableAtFilter Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.IntegrableAtFilter	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Integrable.congr Filter.EventuallyEq.restrict

MeasureTheory.LocallyIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.LocallyIntegrable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.LocallyIntegrable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.IntegrableAtFilter.congr

MeasureTheory.LocallyIntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict MeasureTheory.LocallyIntegrableOn	MeasureTheory.LocallyIntegrableOn	—	MeasureTheory.Measure.instOuterMeasureClass Filter.inter_mem self_mem_nhdsWithin MeasureTheory.Integrable.congr MeasureTheory.IntegrableOn.mono_set Set.inter_subset_right Filter.EventuallyEq.filter_mono MeasureTheory.ae_mono MeasureTheory.Measure.restrict_mono Set.inter_subset_left le_refl

MeasureTheory.Martingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.Martingale MeasureTheory.StronglyAdapted UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Martingale	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.symm MeasureTheory.condExp_congr_ae Filter.EventuallyEq.trans

MeasureTheory.Measure.QuasiMeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Measurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Measure.QuasiMeasurePreserving	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map_congr Filter.EventuallyEq.symm absolutelyContinuous

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.MeasurePreserving Measurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.MeasurePreserving	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map_congr Filter.EventuallyEq.symm map_eq

MeasureTheory.NullMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.NullMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.NullMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass EventuallyMeasurable.congr Filter.EventuallyEq.symm

MeasureTheory.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.NullMeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.NullMeasurableSet	—	MeasureTheory.Measure.instOuterMeasureClass EventuallyMeasurableSet.congr Filter.EventuallyEq.symm

MeasureTheory.Submartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.Submartingale MeasureTheory.StronglyAdapted UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Submartingale	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventuallyLE_congr MeasureTheory.condExp_congr_ae ae_le_condExp MeasureTheory.integrable_congr integrable

MeasureTheory.Supermartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.Supermartingale MeasureTheory.StronglyAdapted UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Supermartingale	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.condExp_congr_ae condExp_ae_le Filter.univ_mem' MeasureTheory.integrable_congr integrable

MeasureTheory.TendstoInDistribution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeasureTheory.IsProbabilityMeasure Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.TendstoInDistribution	MeasureTheory.TendstoInDistribution	—	MeasureTheory.Measure.instOuterMeasureClass AEMeasurable.congr forall_aemeasurable aemeasurable_limit MeasureTheory.Measure.isProbabilityMeasure_map MeasureTheory.Measure.map_congr Filter.EventuallyEq.symm Mathlib.Tactic.DepRewrite.nddcongrArg tendsto

MeasureTheory.TendstoInMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.TendstoInMeasure	MeasureTheory.TendstoInMeasure	—	MeasureTheory.Measure.instOuterMeasureClass congr' Filter.Eventually.of_forall

MeasureTheory.pdf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.pdf	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf_def MeasureTheory.Measure.map_congr

MeromorphicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeromorphicAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl Set.instSingletonSet	MeromorphicAt	—	AnalyticAt.sub analyticAt_id analyticAt_const AnalyticAt.congr AnalyticAt.fun_smul NormedSpace.toIsBoundedSMul IsScalarTower.left Filter.mp_mem eventuallyEq_nhdsWithin_iff Filter.univ_mem' eq_or_ne sub_self zero_smul zero_pow Set.mem_compl_singleton_iff pow_succ' SemigroupAction.mul_smul

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MeromorphicOn Set.EqOn IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	MeromorphicOn	—	MeromorphicAt.congr Filter.EventuallyEq.filter_mono Filter.eventually_of_mem IsOpen.mem_nhds nhdsWithin_le_nhds

Module.Baer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	Module.Baer	—	RingHomInvPair.ids of_equiv

Module.DirectLimit

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_symm_apply_of, congr_apply_of

Module.Dual

Definitions

Name	Category	Theorems
congr 📖	CompOp	4 math math: IsBaseChange.toDual_apply, baseChange_baseChange, congr_apply_apply, congr_symm_apply_apply

Module.Invertible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	Module.Invertible	—	RingHomInvPair.ids right Algebra.to_smulCommClass RingHomCompTriple.ids

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	MonotoneOn Set.EqOn	MonotoneOn	—	—

MulAut

Definitions

Name	Category	Theorems
congr 📖	CompOp	6 math math: SemidirectProduct.congr'_apply_right, SemidirectProduct.congr'_apply_left, SemidirectProduct.congr'_symm_apply_right, SemidirectProduct.congr'_symm_apply_left, congr_apply, congr_symm_apply

Multipliable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Multipliable	Multipliable	—	multipliable_congr

Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	—	—	—	map

PiTensorProduct

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_symm_tprod, congr_tprod

Pregroupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	IsOpen property	property	—	—

ProbabilityTheory.HasGaussianLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ProbabilityTheory.HasGaussianLaw Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.HasGaussianLaw	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map_congr isGaussian_map

ProbabilityTheory.HasLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ProbabilityTheory.HasLaw Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.HasLaw	—	MeasureTheory.Measure.instOuterMeasureClass AEMeasurable.congr aemeasurable Filter.EventuallyEq.symm MeasureTheory.Measure.map_congr map_eq

ProbabilityTheory.HasSubgaussianMGF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ProbabilityTheory.HasSubgaussianMGF Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.HasSubgaussianMGF	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.HasSubgaussianMGF_iff_kernel ProbabilityTheory.Kernel.HasSubgaussianMGF.congr MeasureTheory.ae.congr_simp IsScalarTower.right MeasureTheory.Measure.const_comp MeasureTheory.IsProbabilityMeasure.measure_univ MeasureTheory.Measure.dirac.isProbabilityMeasure one_smul

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ProbabilityTheory.IndepFun Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.IndepFun	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.IndepFun.congr' MeasureTheory.ae_dirac_eq instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Unit.borelSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace

ProbabilityTheory.IsAEKolmogorovProcess

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ProbabilityTheory.IsAEKolmogorovProcess Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.IsAEKolmogorovProcess	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem Filter.univ_mem'

ProbabilityTheory.IsGaussianProcess

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ProbabilityTheory.IsGaussianProcess Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ProbabilityTheory.IsGaussianProcess	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.map_restrict_eq_of_forall_ae_eq Filter.EventuallyEq.symm ProbabilityTheory.HasGaussianLaw.isGaussian_map hasGaussianLaw

ProbabilityTheory.Kernel.HasSubgaussianMGF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	ProbabilityTheory.Kernel.HasSubgaussianMGF Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.HasSubgaussianMGF	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integrable_congr Filter.mp_mem Filter.univ_mem' integrable_exp_mul MeasureTheory.Measure.ae_ae_of_ae_comp Nat.instAtLeastTwoHAddOfNat mgf_le ProbabilityTheory.mgf_congr Filter.EventuallyEq.symm

ProbabilityTheory.Kernel.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.Indep	ProbabilityTheory.Kernel.Indep	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.indep_congr

ProbabilityTheory.Kernel.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.IndepFun	ProbabilityTheory.Kernel.IndepFun	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.indepFun_congr

ProbabilityTheory.Kernel.IndepSets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.IndepSets	ProbabilityTheory.Kernel.IndepSets	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.indepSets_congr

ProbabilityTheory.Kernel.iIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.iIndep	ProbabilityTheory.Kernel.iIndep	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndep_congr

ProbabilityTheory.Kernel.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.iIndepFun	ProbabilityTheory.Kernel.iIndepFun	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepFun_congr

ProbabilityTheory.Kernel.iIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.iIndepSet	ProbabilityTheory.Kernel.iIndepSet	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepSet_congr

ProbabilityTheory.Kernel.iIndepSets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.iIndepSets	ProbabilityTheory.Kernel.iIndepSets	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepSets_congr

ProbabilityTheory.Kernel.indepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.IndepSet	ProbabilityTheory.Kernel.IndepSet	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.indepSet_congr

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.iIndepFun	ProbabilityTheory.iIndepFun	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.iIndepFun_congr

Quot

Definitions

Name	Category	Theorems
congr 📖	CompOp	1 math math: congr_mk

QuotSMulTop

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

Quotient

Definitions

Name	Category	Theorems
congr 📖	CompOp	1 math math: congr_mk

QuotientAddGroup

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

QuotientGroup

Definitions

Name	Category	Theorems
congr 📖	CompOp	9 math math: congr_refl, congr_symm, congr_apply, Submodule.unitsQuotEquivRelPic_symm_apply, ClassGroup.equivPic_symm_apply, congr_mk', congr_mk, ClassGroup.equivPic_apply, Submodule.unitsQuotEquivRelPic_apply_coe

RegularWreathProduct

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

Ring.DirectLimit

Definitions

Name	Category	Theorems
congr 📖	CompOp	2 math math: congr_symm_apply_of, congr_apply_of

RingCon

Definitions

Name	Category	Theorems
congr 📖	CompOp	1 math math: congr_mk

SemidirectProduct

Definitions

Name	Category	Theorems
congr 📖	CompOp	4 math math: congr_symm_apply_left, congr_symm_apply_right, congr_apply_left, congr_apply_right

Set.BijOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Set.BijOn Set.EqOn	Set.BijOn	—	Set.MapsTo.congr mapsTo Set.InjOn.congr injOn Set.SurjOn.congr surjOn

Set.InjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Set.InjOn Set.EqOn	Set.InjOn	—	—

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Set.MapsTo Set.EqOn	Set.MapsTo	—	—

Set.SurjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Set.SurjOn Set.EqOn	Set.SurjOn	—	eq_1 Set.EqOn.image_eq

StrictAntiOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	StrictAntiOn Set.EqOn	StrictAntiOn	—	StrictMonoOn.congr dual_right

StrictConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	StrictConcaveOn Set.EqOn	StrictConcaveOn	—	LT.lt.le

StrictConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	StrictConvexOn Set.EqOn	StrictConvexOn	—	LT.lt.le

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	StrictMonoOn Set.EqOn	StrictMonoOn	—	—

StructureGroupoid.LocalInvariantProp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhds	—	—	congr_iff

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Summable	Summable	—	summable_congr

TendstoLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	TendstoLocallyUniformly	TendstoLocallyUniformly	—	congr_inseparable Filter.Eventually.of_forall Inseparable.of_eq

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	TendstoLocallyUniformlyOn Set.EqOn	TendstoLocallyUniformlyOn	—	congr_inseparable Filter.Eventually.of_forall Inseparable.of_eq

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	TendstoUniformlyOn Filter.Eventually Set.EqOn	TendstoUniformlyOn	—	congr_inseparable Filter.Eventually.mono Inseparable.of_eq

TendstoUniformlyOnFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	TendstoUniformlyOnFilter Filter.Eventually SProd.sprod Filter Filter.instSProd	TendstoUniformlyOnFilter	—	congr_inseparable Filter.Eventually.mono Inseparable.of_eq

TensorProduct

Definitions

Name	Category	Theorems
congr 📖	CompOp	25 math math: congr_symm, congr_congr, congr_zpow, LinearEquiv.rTensor_trans_congr, LinearEquiv.lTensor_trans_congr, congr_refl_refl, congr_trans, AlgebraTensorModule.congr_eq, leftComm_def, congr_tmul, toLinearEquiv_congrIsometry, LinearEquiv.congr_trans_rTensor, congr_symm_tmul, starLinearEquiv_tensor, Equiv.tensorProductAssoc_def, toLinearMap_congr, congr_mul, congr_pow, LinearEquiv.rTensor_trans_lTensor, Submodule.mulMap_op, congrIsometry_apply, Equiv.tensorProductComm_def, LinearEquiv.lTensor_trans_rTensor, rightComm_def, LinearEquiv.congr_trans_lTensor

TensorProduct.AlgebraTensorModule

Definitions

Name	Category	Theorems
congr 📖	CompOp	9 math math: congr_refl, congr_symm, congr_symm_tmul, congr_eq, congr_mul, Algebra.TensorProduct.congr_toLinearEquiv, congr_one, congr_trans, congr_tmul

ULiftable

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	UniformContinuousOn Set.EqOn	UniformContinuousOn	—	Filter.Tendsto.congr' Filter.EventuallyEq.filter_mono Filter.mp_mem Filter.mem_principal_self Filter.univ_mem' inf_le_right

Valuation

Definitions

Name	Category	Theorems
congr 📖	CompOp	—

WithAbs

Definitions

Name	Category	Theorems
congr 📖	CompOp	12 math math: AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs, congr_refl, congr_symm_apply, AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero, congr_apply, equivWithAbs_equiv_symm_apply, equiv_equivWithAbs_symm_apply, congr_trans, congr_symm, equivWithAbs_symm, AbsoluteValue.isEquiv_iff_isHomeomorph, equivWithAbs_symm_equiv_symm_apply

WithConv

Definitions

Name	Category	Theorems
congr 📖	CompOp	4 math math: symm_congr_apply, toEquiv_congrLinearEquiv, symm_congr, congr_apply

WithLp

Definitions

Name	Category	Theorems
congr 📖	CompOp	4 math math: congr_refl, coe_congr, congr_trans, congr_symm

WithSeminorms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	WithSeminorms Seminorm.IsBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing RingHomIsometric.ids LinearMap.id AddCommGroup.toAddCommMonoid	WithSeminorms	—	RingHomIsometric.ids topology_eq_withSeminorms le_antisymm continuous_id_iff_le continuous_of_isBounded

WithVal

Definitions

Name	Category	Theorems
congr 📖	CompOp	10 math math: congr_symm_apply, Valuation.IsEquiv.uniformContinuous_equivWithVal, equivWithVal_symm, Valuation.IsEquiv.uniformContinuous_congr, congr_apply, congr_symm, equivWithVal_apply, congr_refl, equivWithVal_symm_apply, congr_trans

eVariationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	Set.EqOn	eVariationOn	—	—

groupCohomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quiver.Hom Rep CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.res	—	—

groupHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quiver.Hom Rep CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.res	—	—

---

← Back to Index