Congr

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Congr.lean

Statistics

Metric	Count
Definitions	0
Theorems congr_of_eventuallyEq, congr_mono, congr_mono, congr_of_eventuallyEq, congr_of_eventuallyEq_insert, congr_of_eventuallyEq_of_mem, fderivWithin_congr_mono, differentiableAt_iff, differentiableWithinAt_iff, differentiableWithinAt_iff_of_mem, fderiv, fderivWithin, fderivWithin', fderivWithin_eq, fderivWithin_eq_of_insert, fderivWithin_eq_of_mem, fderivWithin_eq_of_nhds, fderiv_eq, hasFDerivAtFilter_iff, hasFDerivAt_iff, hasFDerivWithinAt_iff, hasFDerivWithinAt_iff_of_mem, hasStrictFDerivAt_iff, congr_fderiv, congr_of_eventuallyEq, congr_of_eventuallyEq, congr', congr_fderiv, congr_mono, congr_of_eventuallyEq, congr_fderiv, congr_of_eventuallyEq, differentiableOn_congr, differentiableWithinAt_congr_set, differentiableWithinAt_congr_set', differentiableWithinAt_congr_set_nhdsNE, fderivWithin_congr, fderivWithin_congr', fderivWithin_congr_set, fderivWithin_congr_set', fderivWithin_congr_set_nhdsNE, fderivWithin_eventually_congr_set, fderivWithin_eventually_congr_set', hasFDerivWithinAt_congr_set, hasFDerivWithinAt_congr_set', hasFDerivWithinAt_congr_set_nhdsNE	46
Total	46

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_of_eventuallyEq 📖	—	DifferentiableAt Filter.EventuallyEq nhds	—	—	Filter.EventuallyEq.differentiableAt_iff

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_mono 📖	—	DifferentiableOn Set Set.instHasSubset	—	—	DifferentiableWithinAt.congr_mono

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_mono 📖	—	DifferentiableWithinAt Set.EqOn Set Set.instHasSubset	—	—	HasFDerivWithinAt.differentiableWithinAt HasFDerivWithinAt.congr_mono hasFDerivWithinAt
congr_of_eventuallyEq 📖	—	DifferentiableWithinAt Filter.EventuallyEq nhdsWithin	—	—	HasFDerivWithinAt.differentiableWithinAt HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt
congr_of_eventuallyEq_insert 📖	—	DifferentiableWithinAt Filter.EventuallyEq nhdsWithin Set Set.instInsert	—	—	of_insert congr_of_eventuallyEq_of_mem insert Set.mem_insert
congr_of_eventuallyEq_of_mem 📖	—	DifferentiableWithinAt Filter.EventuallyEq nhdsWithin Set Set.instMembership	—	—	congr_of_eventuallyEq mem_of_mem_nhdsWithin
fderivWithin_congr_mono 📖	mathematical	DifferentiableWithinAt Set.EqOn UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Set Set.instHasSubset	fderivWithin	—	HasFDerivWithinAt.fderivWithin HasFDerivWithinAt.congr_mono hasFDerivWithinAt

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_iff 📖	mathematical	Filter.EventuallyEq nhds	DifferentiableAt	—	hasFDerivAt_iff
differentiableWithinAt_iff 📖	mathematical	Filter.EventuallyEq nhdsWithin	DifferentiableWithinAt	—	hasFDerivWithinAt_iff
differentiableWithinAt_iff_of_mem 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instMembership	DifferentiableWithinAt	—	differentiableWithinAt_iff eq_of_nhdsWithin
fderiv 📖	mathematical	Filter.EventuallyEq nhds	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderiv	—	Filter.Eventually.mono eventuallyEq_nhds fderiv_eq
fderivWithin 📖	mathematical	Filter.EventuallyEq nhdsWithin	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderivWithin	—	fderivWithin' Set.Subset.rfl
fderivWithin' 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instHasSubset	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderivWithin	—	Filter.Eventually.mp eventually_eventually_nhdsWithin Filter.Eventually.mono eventually_mem_nhdsWithin fderivWithin_eq Filter.Eventually.filter_mono nhdsWithin_mono Filter.Eventually.self_of_nhdsWithin
fderivWithin_eq 📖	mathematical	Filter.EventuallyEq nhdsWithin	fderivWithin	—	hasFDerivWithinAt_iff fderivWithin_def
fderivWithin_eq_of_insert 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instInsert	fderivWithin	—	fderivWithin_eq nhdsWithin_mono Set.subset_insert mem_of_mem_nhdsWithin Set.mem_insert
fderivWithin_eq_of_mem 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instMembership	fderivWithin	—	fderivWithin_eq mem_of_mem_nhdsWithin
fderivWithin_eq_of_nhds 📖	mathematical	Filter.EventuallyEq nhds	fderivWithin	—	fderivWithin_eq filter_mono nhdsWithin_le_nhds Filter.Eventually.self_of_nhds
fderiv_eq 📖	mathematical	Filter.EventuallyEq nhds	fderiv	—	fderivWithin_univ fderivWithin_eq_of_nhds
hasFDerivAtFilter_iff 📖	mathematical	Filter.EventuallyEq DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	HasFDerivAtFilter	—	Asymptotics.isLittleOTVS_congr Filter.Eventually.mono rfl
hasFDerivAt_iff 📖	mathematical	Filter.EventuallyEq nhds	HasFDerivAt	—	hasFDerivAtFilter_iff eq_of_nhds
hasFDerivWithinAt_iff 📖	mathematical	Filter.EventuallyEq nhdsWithin	HasFDerivWithinAt	—	hasFDerivAtFilter_iff
hasFDerivWithinAt_iff_of_mem 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instMembership	HasFDerivWithinAt	—	hasFDerivWithinAt_iff eq_of_nhdsWithin
hasStrictFDerivAt_iff 📖	mathematical	Filter.EventuallyEq nhds DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	HasStrictFDerivAt	—	hasStrictFDerivAt_iff_isLittleOTVS Asymptotics.isLittleOTVS_congr Filter.Eventually.mono Filter.Eventually.prodMk_nhds rfl

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_fderiv 📖	—	HasFDerivAt	—	—	—
congr_of_eventuallyEq 📖	—	HasFDerivAt Filter.EventuallyEq nhds	—	—	HasFDerivAtFilter.congr_of_eventuallyEq mem_of_mem_nhds

HasFDerivAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_of_eventuallyEq 📖	—	HasFDerivAtFilter Filter.EventuallyEq	—	—	Filter.EventuallyEq.hasFDerivAtFilter_iff

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr' 📖	—	HasFDerivWithinAt Set.EqOn Set Set.instMembership	—	—	congr
congr_fderiv 📖	—	HasFDerivWithinAt	—	—	—
congr_mono 📖	—	HasFDerivWithinAt Set.EqOn Set Set.instHasSubset	—	—	HasFDerivAtFilter.congr_of_eventuallyEq mono Filter.mem_inf_of_right
congr_of_eventuallyEq 📖	—	HasFDerivWithinAt Filter.EventuallyEq nhdsWithin	—	—	HasFDerivAtFilter.congr_of_eventuallyEq

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_fderiv 📖	—	HasStrictFDerivAt	—	—	—
congr_of_eventuallyEq 📖	—	HasStrictFDerivAt Filter.EventuallyEq nhds	—	—	Filter.EventuallyEq.hasStrictFDerivAt_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableOn_congr 📖	mathematical	—	DifferentiableOn	—	DifferentiableOn.congr
differentiableWithinAt_congr_set 📖	mathematical	Filter.EventuallyEq nhds	DifferentiableWithinAt	—	hasFDerivWithinAt_congr_set
differentiableWithinAt_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	DifferentiableWithinAt	—	hasFDerivWithinAt_congr_set'
differentiableWithinAt_congr_set_nhdsNE 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	DifferentiableWithinAt	—	hasFDerivWithinAt_congr_set_nhdsNE
fderivWithin_congr 📖	mathematical	Set.EqOn	fderivWithin	—	Filter.EventuallyEq.fderivWithin_eq Filter.EventuallyEq.filter_mono Set.EqOn.eventuallyEq inf_le_right
fderivWithin_congr' 📖	mathematical	Set.EqOn Set Set.instMembership	fderivWithin	—	fderivWithin_congr
fderivWithin_congr_set 📖	mathematical	Filter.EventuallyEq nhds	fderivWithin	—	fderivWithin_congr_set_nhdsNE Filter.EventuallyEq.filter_mono inf_le_left
fderivWithin_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	fderivWithin	—	differentiableWithinAt_congr_set' hasFDerivWithinAt_congr_set' fderivWithin_def
fderivWithin_congr_set_nhdsNE 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	fderivWithin	—	differentiableWithinAt_congr_set_nhdsNE hasFDerivWithinAt_congr_set_nhdsNE fderivWithin_def
fderivWithin_eventually_congr_set 📖	mathematical	Filter.EventuallyEq nhds	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderivWithin	—	Filter.Eventually.mono eventually_eventually_nhds fderivWithin_congr_set
fderivWithin_eventually_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid nhds fderivWithin	—	Filter.Eventually.mono eventually_nhds_nhdsWithin fderivWithin_congr_set'
hasFDerivWithinAt_congr_set 📖	mathematical	Filter.EventuallyEq nhds	HasFDerivWithinAt	—	hasFDerivWithinAt_congr_set_nhdsNE Filter.EventuallyEq.filter_mono inf_le_left
hasFDerivWithinAt_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	HasFDerivWithinAt	—	eq_or_ne hasFDerivWithinAt_congr_set_nhdsNE hasFDerivWithinAt_congr_set Ne.nhdsWithin_compl_singleton
hasFDerivWithinAt_congr_set_nhdsNE 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	HasFDerivWithinAt	—	hasFDerivWithinAt_diff_singleton_self Set.inter_comm

---

← Back to Index