Commit 2024-02-26 23:59 162edaa4

View on Github →

feat: lemmas about germs in topological spaces (#9747) From sphere-eversion; I'm just upstreaming it. Co-authored by: @PatrickMassot (original author)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.EventuallyEq.comp_tendsto

Modified Mathlib/Order/Filter/Germ.lean

deleted theorem Filter.EventuallyEq.comp_tendsto

added theorem Filter.Germ.Filter.Tendsto.congr_germ

added def Filter.Germ.IsConstant

added theorem Filter.Germ.isConstant_coe

added theorem Filter.Germ.isConstant_coe_const

added theorem Filter.Germ.isConstant_comp

added theorem Filter.Germ.isConstant_compTendsto

added theorem Filter.Germ.isConstant_comp_tendsto

Modified Mathlib/RingTheory/Subring/Order.lean

added def Subring.orderedSubtype

added theorem Subring.orderedSubtype_coe

Created Mathlib/Topology/Germ.lean

added theorem Filter.Eventually.germ_congr_set

added theorem Filter.Germ.isConstant_comp_subtype

added def Filter.Germ.sliceLeft

added theorem Filter.Germ.sliceLeft_coe

added def Filter.Germ.sliceRight

added theorem Filter.Germ.sliceRight_coe

added def Filter.Germ.value

added def Filter.Germ.valueMulHom

added def Filter.Germ.valueOrderRingHom

added def Filter.Germ.valueRingHom

added theorem Filter.Germ.value_smul

added def Filter.Germ.valueₗ

added theorem Germ.coe_prod

added theorem IsLocallyConstant.of_germ_isConstant

added def RestrictGermPredicate

added theorem eq_of_germ_isConstant

added theorem eq_of_germ_isConstant_on

added theorem forall_restrictGermPredicate_iff

added theorem forall_restrictGermPredicate_of_forall

added theorem restrictGermPredicate_congr

Modified scripts/noshake.json