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	34
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	144
Total	178

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	AEMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	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 📖	—	AnalyticAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	—	HasFPowerSeriesAt.analyticAt HasFPowerSeriesAt.congr

AnalyticOn

Theorems

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

AnalyticOnNhd

Theorems

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

AnalyticWithinAt

Theorems

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

AntitoneOn

Theorems

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

Asymptotics.IsBigO

Theorems

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

Asymptotics.IsBigOTVS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	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 📖	—	Asymptotics.IsBigOWith	—	—	congr' Filter.univ_mem'

Asymptotics.IsLittleO

Theorems

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

Asymptotics.IsLittleOTVS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	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 📖	—	Asymptotics.SuperpolynomialDecay	—	—	Filter.Tendsto.congr

BaireMeasurableSet

Theorems

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

CPolynomialAt

Theorems

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

CPolynomialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup CPolynomialOn Set.EqOn	—	—	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 📖	—	ConcaveOn Set.EqOn	—	—	—

ConformalAt

Theorems

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

ContDiffOn

Theorems

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

ContDiffWithinAt

Theorems

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

ContMDiff

Theorems

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

ContMDiffOn

Theorems

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

ContMDiffWithinAt

Theorems

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

Continuous

Theorems

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

ContinuousAt

Theorems

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

ContinuousLinearMap.HasLeftInverse

Theorems

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

ContinuousLinearMap.HasRightInverse

Theorems

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

ContinuousOn

Theorems

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

ContinuousWithinAt

Theorems

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

ConvexOn

Theorems

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

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 📖	—	DifferentiableOn	—	—	DifferentiableWithinAt.congr

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	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 📖	—	EventuallyMeasurable Filter.EventuallyEq	—	—	EventuallyMeasurableSet.congr Filter.EventuallyEq.preimage

EventuallyMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	EventuallyMeasurableSet Filter.EventuallyEq	—	—	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 📖	—	Filter.Eventually	—	—	mp mono

Filter.EventuallyConst

Theorems

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

Filter.EventuallyLE

Theorems

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

Filter.HasBasis

Theorems

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

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	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

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	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 📖	—	HasFDerivWithinAt Set.EqOn	—	—	congr_mono Set.Subset.refl

HasFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	HasFPowerSeriesAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	—	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 📖	—	HasFPowerSeriesOnBall Set.EqOn Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	—	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 📖	—	HasFPowerSeriesWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	—	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 📖	—	HasFPowerSeriesWithinOnBall Set.EqOn Set Set.instInter Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	—	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 📖	—	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 📖	—	HasFiniteFPowerSeriesAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	—	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 📖	—	HasFiniteFPowerSeriesOnBall Set.EqOn Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	—	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 📖	—	HasGradientWithinAt	—	—	congr_mono

HasLineDerivWithinAt

Theorems

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

HasProdUniformly

Theorems

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

HasProdUniformlyOn

Theorems

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

HasSumUniformly

Theorems

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

HasSumUniformlyOn

Theorems

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

IntervalIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	Set.EqOn Real Set.uIoc Real.linearOrder 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 📖	—	IsExtrFilter Filter.EventuallyEq	—	—	eq_1 Filter.EventuallyEq.isMaxFilter_iff Filter.EventuallyEq.isMinFilter_iff

IsLocalExtr

Theorems

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

IsLocalExtrOn

Theorems

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

IsLocalFrameOn

Theorems

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

IsLocalMax

Theorems

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

IsLocalMaxOn

Theorems

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

IsLocalMin

Theorems

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

IsLocalMinOn

Theorems

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

IsMaxFilter

Theorems

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

IsMinFilter

Theorems

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

IsMulFreimanHom

Theorems

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

IsMulFreimanIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	IsMulFreimanIso Set.EqOn	—	—	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 📖	—	LineDifferentiableWithinAt	—	—	congr_mono Set.Subset.refl

LinearIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	LinearIndepOn Set.EqOn	—	—	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	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	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	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	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 📖	—	MDifferentiableOn	—	—	StructureGroupoid.LocalInvariantProp.liftPropOn_congr differentiableWithinAt_localInvariantProp

MDifferentiableWithinAt

Theorems

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

Manifold.IsImmersion

Theorems

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

Manifold.IsImmersionOfComplement

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	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 📖	—	MeasurableSet	—	—	—

MeasureTheory.AEDisjoint

Theorems

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

MeasureTheory.AEStronglyMeasurable

Theorems

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

MeasureTheory.HasFiniteIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	MeasureTheory.HasFiniteIntegral Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	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 📖	—	MeasureTheory.Integrable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEStronglyMeasurable.congr MeasureTheory.HasFiniteIntegral.congr

MeasureTheory.NullMeasurable

Theorems

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

MeasureTheory.NullMeasurableSet

Theorems

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

MeasureTheory.TendstoInMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass 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 📖	—	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	—	—	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 📖	—	MeromorphicOn Set.EqOn IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	—	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 📖	—	MonotoneOn Set.EqOn	—	—	—

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 📖	—	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 📖	—	IsOpen property	—	—	—

ProbabilityTheory.HasGaussianLaw

Theorems

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

ProbabilityTheory.HasLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	ProbabilityTheory.HasLaw Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	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 📖	—	ProbabilityTheory.HasSubgaussianMGF Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	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 📖	—	ProbabilityTheory.IndepFun Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	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 📖	—	ProbabilityTheory.IsAEKolmogorovProcess Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem Filter.univ_mem'

ProbabilityTheory.IsGaussianProcess

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	ProbabilityTheory.IsGaussianProcess Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	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 📖	—	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	—	—	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 📖	—	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.Indep	—	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.indep_congr

ProbabilityTheory.Kernel.IndepFun

Theorems

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

ProbabilityTheory.Kernel.IndepSets

Theorems

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

ProbabilityTheory.Kernel.iIndep

Theorems

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

ProbabilityTheory.Kernel.iIndepFun

Theorems

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

ProbabilityTheory.Kernel.iIndepSet

Theorems

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

ProbabilityTheory.Kernel.iIndepSets

Theorems

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

ProbabilityTheory.Kernel.indepSet

Theorems

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

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass 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 📖	—	Set.BijOn Set.EqOn	—	—	Set.MapsTo.congr mapsTo Set.InjOn.congr injOn Set.SurjOn.congr surjOn

Set.InjOn

Theorems

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

Set.MapsTo

Theorems

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

Set.SurjOn

Theorems

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

StrictAntiOn

Theorems

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

StrictConcaveOn

Theorems

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

StrictConvexOn

Theorems

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

StrictMonoOn

Theorems

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

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 📖	—	Summable	—	—	summable_congr

TendstoLocallyUniformly

Theorems

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

TendstoLocallyUniformlyOn

Theorems

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

TendstoUniformlyOn

Theorems

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

TendstoUniformlyOnFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	—	TendstoUniformlyOnFilter Filter.Eventually SProd.sprod Filter Filter.instSProd	—	—	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 📖	—	UniformContinuousOn Set.EqOn	—	—	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	—

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 📖	—	WithSeminorms Seminorm.IsBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing RingHomIsometric.ids LinearMap.id AddCommGroup.toAddCommMonoid	—	—	RingHomIsometric.ids topology_eq_withSeminorms le_antisymm continuous_id_iff_le Seminorm.continuous_from_bounded

groupCohomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quiver.Hom Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res	—	—

groupHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr 📖	mathematical	—	MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quiver.Hom Rep CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.res	—	—

---

← Back to Index