Germ

📁 Source: Mathlib/Topology/Germ.lean

Statistics

Metric	Count
Definitions Germ, sliceLeft, sliceRight, value, valueAddHom, valueMulHom, valueOrderRingHom, valueRingHom, valueₗ, RestrictGermPredicate	10
Theorems germ_congr_set, isConstant_comp_subtype, sliceLeft_coe, sliceRight_coe, value_smul, coe_prod, coe_sum, of_germ_isConstant, eq_of_germ_isConstant, eq_of_germ_isConstant_on, forall_restrictGermPredicate_iff, forall_restrictGermPredicate_of_forall, restrictGermPredicate_congr	13
Total	23

Filter

Definitions

Name	Category	Theorems
Germ 📖	CompOp	86 math math: Germ.coe_coeMulHom, Germ.instIsCancelAdd, Germ.const_ofNat, Germ.const_neg, Germ.instIsLeftCancelAdd, MeasureTheory.AEEqFun.toGerm_injective, Germ.const_nat, MeasureTheory.AEEqFun.neg_toGerm, Germ.coe_nonneg, Germ.coe_lt, Germ.const_top, Germ.instIsOrderedAddMonoid, Germ.coe_one, Germ.instCanonicallyOrderedAdd, Germ.coe_prod, Germ.instIsOrderedRing, Germ.instCanonicallyOrderedMul, Germ.map_id, Germ.lt_def, Germ.total, Germ.coe_vadd', Germ.coe_nsmul, Germ.instIsOrderedCancelMonoid, Germ.instIsCancelMul, Germ.le_def, Germ.const_inv, Germ.value_smul, Germ.const_smul, Germ.coe_sub, Germ.coe_pos, MeasureTheory.AEEqFun.smul_toGerm, Germ.instNontrivial, Germ.coe_smul, Germ.coe_sum, MeasureTheory.AEEqFun.pow_toGerm, Germ.const_sub, Germ.coe_coeAddHom, MeasureTheory.AEEqFun.toGermMonoidHom_apply, Germ.coe_le, MeasureTheory.AEEqFun.one_toGerm, Germ.const_le_iff, Germ.instExistsAddOfLE, Germ.coe_neg, Germ.instExistsMulOfLE, Germ.coe_coeRingHom, Germ.const_abs, Germ.const_vadd, Germ.coe_div, Germ.const_pow, MeasureTheory.AEEqFun.sub_toGerm, Germ.coe_add, Germ.coe_zero, MeasureTheory.AEEqFun.toGermAddMonoidHom_apply, Germ.coe_inv, MeasureTheory.AEEqFun.div_toGerm, Germ.const_max, Germ.instIsLeftCancelMul, Germ.instIsRightCancelAdd, Germ.coe_smul', Germ.natCast_def, Germ.coe_vadd, Germ.instIsRightCancelMul, Germ.const_inf, MeasureTheory.AEEqFun.mul_toGerm, MeasureTheory.AEEqFun.zpow_toGerm, Germ.const_sup, Germ.instIsOrderedAddCancelMonoid, Germ.const_min, MeasureTheory.AEEqFun.zero_toGerm, Germ.const_lt, Germ.const_div, Germ.coe_ofNat, Germ.min_def, Germ.const_le, Germ.const_bot, Germ.coe_pow, Germ.max_def, Germ.intCast_def, Germ.coe_mul, Germ.abs_def, Germ.instIsStrictOrderedRing, MeasureTheory.AEEqFun.inv_toGerm, MeasureTheory.AEEqFun.add_toGerm, Germ.const_lt_iff, Germ.const_nsmul, Germ.instIsOrderedMonoid

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
germ_congr_set 📖	—	Filter.Eventually Filter.Germ.ofFun nhds nhdsSet	—	—	eventually_nhdsSet_iff_forall mono and eventually_nhds Filter.Germ.coe_eq

Filter.Germ

Definitions

Name	Category	Theorems
sliceLeft 📖	CompOp	1 math math: sliceLeft_coe
sliceRight 📖	CompOp	1 math math: sliceRight_coe
value 📖	CompOp	1 math math: value_smul
valueAddHom 📖	CompOp	—
valueMulHom 📖	CompOp	—
valueOrderRingHom 📖	CompOp	—
valueRingHom 📖	CompOp	—
valueₗ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConstant_comp_subtype 📖	mathematical	IsConstant nhds Set Set.instMembership ofFun	Set.Elem instTopologicalSpaceSubtype	—	isConstant_comp_tendsto continuousAt_subtype_val
sliceLeft_coe 📖	mathematical	—	sliceLeft ofFun nhds instTopologicalSpaceProd	—	—
sliceRight_coe 📖	mathematical	—	sliceRight ofFun nhds instTopologicalSpaceProd	—	—
value_smul 📖	mathematical	—	value Filter.Germ nhds instSMul'	—	inductionOn

Germ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_prod 📖	mathematical	—	Filter.Germ.ofFun Finset.prod Pi.commMonoid Filter.Germ Filter.Germ.instCommMonoid	—	map_prod MonoidHom.instMonoidHomClass
coe_sum 📖	mathematical	—	Filter.Germ.ofFun Finset.sum Pi.addCommMonoid Filter.Germ Filter.Germ.instAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass

IsLocallyConstant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_germ_isConstant 📖	mathematical	Filter.Germ.IsConstant nhds Filter.Germ.ofFun	IsLocallyConstant	—	isOpen_iff_mem_nhds Filter.mem_of_superset mem_of_mem_nhds Set.mem_preimage

(root)

Definitions

Name	Category	Theorems
RestrictGermPredicate 📖	MathDef	2 math math: forall_restrictGermPredicate_iff, forall_restrictGermPredicate_of_forall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_germ_isConstant 📖	—	Filter.Germ.IsConstant nhds Filter.Germ.ofFun	—	—	IsLocallyConstant.apply_eq_of_isPreconnected IsLocallyConstant.of_germ_isConstant preconnectedSpace_iff_univ
eq_of_germ_isConstant_on 📖	—	Filter.Germ.IsConstant nhds Filter.Germ.ofFun IsPreconnected Set Set.instMembership	—	—	Subtype.preconnectedSpace eq_of_germ_isConstant Filter.Germ.isConstant_comp_subtype
forall_restrictGermPredicate_iff 📖	mathematical	—	RestrictGermPredicate Filter.Germ.ofFun nhds Filter.Eventually nhdsSet	—	eventually_nhdsSet_iff_forall
forall_restrictGermPredicate_of_forall 📖	mathematical	Filter.Germ.ofFun nhds	RestrictGermPredicate	—	forall_restrictGermPredicate_iff Filter.Eventually.of_forall
restrictGermPredicate_congr 📖	—	RestrictGermPredicate Filter.Germ.ofFun nhds Filter.Eventually nhdsSet	—	—	Filter.Eventually.mono Filter.Eventually.and Filter.Eventually.eventually_nhds eventually_nhdsSet_iff_forall Filter.Germ.coe_eq

---

← Back to Index