FiberwiseLinear

📁 Source: Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

Statistics

Metric	Count
Definitions openPartialHomeomorph, contMDiffFiberwiseLinear	2
Theorems locality_aux₁, locality_aux₂, source_trans_PartialHomeomorph, source_trans_openPartialHomeomorph, target_trans_PartialHomeomorph, target_trans_openPartialHomeomorph, trans_PartialHomeomorph_apply, trans_openPartialHomeomorph_apply, mem_contMDiffFiberwiseLinear_iff	9
Total	11

ContMDiffFiberwiseLinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locality_aux₁ 📖	mathematical	IsOpen instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership OpenPartialHomeomorph.EqOnSource OpenPartialHomeomorph.restr FiberwiseLinear.openPartialHomeomorph ContMDiffOn.continuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv SProd.sprod Set.instSProd Set.univ	—	RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup ContMDiffOn.continuousOn OpenPartialHomeomorph.restr_source' Subtype.prop HasSubset.Subset.antisymm Set.instAntisymmSubset OpenPartialHomeomorph.restr_source_inter SetCoe.forall'
locality_aux₂ 📖	—	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set Set.instSProd Set.univ OpenPartialHomeomorph.EqOnSource OpenPartialHomeomorph.restr FiberwiseLinear.openPartialHomeomorph ContMDiffOn.continuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	—	—	RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup ContMDiffOn.continuousOn ContinuousLinearEquiv.ext Set.ext Set.mem_iUnion isOpen_iUnion Eq.le contMDiffOn_of_locally_contMDiffOn ContMDiffOn.mono ContMDiffOn.congr Set.inter_subset_right SetCoe.forall'

FiberwiseLinear

Definitions

Name	Category	Theorems
openPartialHomeomorph 📖	CompOp	7 math math: trans_openPartialHomeomorph_apply, source_trans_PartialHomeomorph, target_trans_openPartialHomeomorph, target_trans_PartialHomeomorph, trans_PartialHomeomorph_apply, source_trans_openPartialHomeomorph, mem_contMDiffFiberwiseLinear_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
source_trans_PartialHomeomorph 📖	mathematical	IsOpen ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd OpenPartialHomeomorph.trans openPartialHomeomorph SProd.sprod Set Set.instSProd Set.instInter Set.univ	—	source_trans_openPartialHomeomorph
source_trans_openPartialHomeomorph 📖	mathematical	IsOpen ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd OpenPartialHomeomorph.trans openPartialHomeomorph SProd.sprod Set Set.instSProd Set.instInter Set.univ	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup Set.ext
target_trans_PartialHomeomorph 📖	mathematical	IsOpen ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd OpenPartialHomeomorph.trans openPartialHomeomorph SProd.sprod Set Set.instSProd Set.instInter Set.univ	—	target_trans_openPartialHomeomorph
target_trans_openPartialHomeomorph 📖	mathematical	IsOpen ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd OpenPartialHomeomorph.trans openPartialHomeomorph SProd.sprod Set Set.instSProd Set.instInter Set.univ	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup Set.ext
trans_PartialHomeomorph_apply 📖	mathematical	IsOpen ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.trans openPartialHomeomorph DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	trans_openPartialHomeomorph_apply
trans_openPartialHomeomorph_apply 📖	mathematical	IsOpen ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.trans openPartialHomeomorph DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup

(root)

Definitions

Name	Category	Theorems
contMDiffFiberwiseLinear 📖	CompOp	2 math math: ContMDiffFiberwiseLinear.hasGroupoid, mem_contMDiffFiberwiseLinear_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_contMDiffFiberwiseLinear_iff 📖	mathematical	—	OpenPartialHomeomorph instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid contMDiffFiberwiseLinear OpenPartialHomeomorph.EqOnSource FiberwiseLinear.openPartialHomeomorph ContMDiffOn.continuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm	—	—

---

← Back to Index