Projection

📁 Source: Mathlib/Geometry/Euclidean/Projection.lean

Statistics

Metric	Count
Definitions orthogonalProjectionSpan, orthogonalProjection, reflection	3
Theorems coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, orthogonalProjectionSpan_congr, orthogonalProjectionSpan_eq_point, orthogonalProjectionSpan_faceOpposite_eq_point_rev, orthogonalProjectionSpan_map, orthogonalProjectionSpan_reindex, orthogonalProjectionSpan_restrict, orthogonalProjection_vadd_smul_vsub_orthogonalProjection, coe_orthogonalProjection_eq_iff_mem, dist_eq_iff_dist_orthogonalProjection_eq, dist_orthogonalProjection_eq_dist_iff_eq_of_mem, dist_orthogonalProjection_eq_infDist, dist_orthogonalProjection_eq_infNndist, dist_orthogonalProjection_eq_zero_iff, dist_orthogonalProjection_ne_zero_of_notMem, dist_reflection, dist_reflection_eq_of_mem, dist_set_eq_iff_dist_orthogonalProjection_eq, dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd, eq_orthogonalProjection_of_eq_subspace, eq_reflection_of_eq_subspace, exists_dist_eq_iff_exists_dist_orthogonalProjection_eq, inter_eq_singleton_orthogonalProjection, orthogonalProjection_affineSpan_singleton, orthogonalProjection_apply, orthogonalProjection_apply', orthogonalProjection_apply_mem, orthogonalProjection_congr, orthogonalProjection_contLinear, orthogonalProjection_eq_iff_mem, orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, orthogonalProjection_eq_self_iff, orthogonalProjection_linear, orthogonalProjection_map, orthogonalProjection_mem, orthogonalProjection_mem_orthogonal, orthogonalProjection_mem_subspace_eq_self, orthogonalProjection_orthogonalProjection, orthogonalProjection_orthogonalProjection_of_le, orthogonalProjection_subtype, orthogonalProjection_sup_of_orthogonalProjection_eq, orthogonalProjection_vadd_eq_self, orthogonalProjection_vadd_smul_vsub_orthogonalProjection, orthogonalProjection_vsub_mem_direction, orthogonalProjection_vsub_mem_direction_orthogonal, orthogonalProjection_vsub_orthogonalProjection, reflection_apply, reflection_apply', reflection_apply_of_mem, reflection_eq_iff_orthogonalProjection_eq, reflection_eq_self_iff, reflection_involutive, reflection_map, reflection_mem_of_le_of_mem, reflection_orthogonal_vadd, reflection_reflection, reflection_subtype, reflection_symm, reflection_vadd_smul_vsub_orthogonalProjection, vsub_orthogonalProjection_mem_direction, vsub_orthogonalProjection_mem_direction_orthogonal	63
Total	66

Affine.Simplex

Definitions

Name	Category	Theorems
orthogonalProjectionSpan 📖	CompOp	17 math math: orthogonalProjectionSpan_map, orthogonalProjection_vadd_smul_vsub_orthogonalProjection, orthogonalProjectionSpan_eq_point, dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, signedInfDist_apply_self, orthogonalProjectionSpan_congr, orthogonalProjection_circumcenter, exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, orthogonalProjection_eq_circumcenter_of_exists_dist_eq, orthogonalProjectionSpan_faceOpposite_eq_point_rev, orthogonalProjectionSpan_restrict, orthogonalProjection_eq_circumcenter_of_dist_eq, coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, abs_signedInfDist_eq_dist_of_mem_affineSpan_range, orthogonalProjectionSpan_reindex, orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, signedInfDist_affineCombination

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange orthogonalProjection_vadd_smul_vsub_orthogonalProjection
dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points	Real Real.instMul Dist.dist PseudoMetricSpace.toDist Real.instAdd DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan	—	EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq
orthogonalProjectionSpan_congr 📖	mathematical	Set.range points NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan	—	EuclideanGeometry.orthogonalProjection_congr
orthogonalProjectionSpan_eq_point 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange orthogonalProjectionSpan.eq_1 Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_singleton EuclideanGeometry.orthogonalProjection_congr EuclideanGeometry.orthogonalProjection_affineSpan_singleton
orthogonalProjectionSpan_faceOpposite_eq_point_rev 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange orthogonalProjectionSpan_eq_point faceOpposite_point_eq_point_rev
orthogonalProjectionSpan_map 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points map SeminormedAddCommGroup.toAddCommGroup AffineIsometry.toAffineMap AffineIsometry.injective DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan AffineIsometry AffineIsometry.instFunLike	—	AffineIsometry.injective instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineSubspace.nonempty_map Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_map finiteDimensional_direction_affineSpan_range Finite.of_fintype EuclideanGeometry.orthogonalProjection_congr AffineIsometry.coe_toAffineMap Set.range_comp AffineSubspace.map_span Set.image_congr EuclideanGeometry.orthogonalProjection_map
orthogonalProjectionSpan_reindex 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points reindex DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan	—	orthogonalProjectionSpan_congr reindex_range_points
orthogonalProjectionSpan_restrict 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	SetLike.instMembership AffineSubspace.instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor Nonempty.map DFunLike.coe AffineMap Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict ContinuousAffineMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toAddCommGroup instTopologicalSpaceSubtype ContinuousAffineMap.instFunLike orthogonalProjectionSpan	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.injective orthogonalProjectionSpan_map
orthogonalProjection_vadd_smul_vsub_orthogonalProjection 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange ContinuousAffineMap.instFunLike orthogonalProjectionSpan HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection

EuclideanGeometry

Definitions

Name	Category	Theorems
orthogonalProjection 📖	CompOp	58 math math: vsub_orthogonalProjection_mem_direction_orthogonal, orthogonalProjection_congr, orthogonalProjection_contLinear, dist_orthogonalProjection_eq_iff_oangle_eq, reflection_vadd_smul_vsub_orthogonalProjection, inter_eq_singleton_orthogonalProjection, orthogonalProjection_map, angle_orthogonalProjection_self, orthogonalProjection_apply_mem, dist_orthogonalProjection_eq_iff_angle_eq, orthogonalProjection_apply', orthogonalProjection_orthogonalProjection_of_le, Sphere.isTangent_iff_isTangentAt_orthogonalProjection, AffineSubspace.signedInfDist_eq_signedDist_of_mem, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, orthogonalProjection_subtype, two_zsmul_oangle_self_orthogonalProjection, orthogonalProjection_vadd_eq_self, oangle_orthogonalProjection_self, dist_orthogonalProjection_eq_dist_iff_eq_of_mem, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, orthogonalProjection_affineSpan_singleton, dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, orthogonalProjection_vadd_smul_vsub_orthogonalProjection, dist_orthogonalProjection_eq_infNndist, Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, dist_eq_iff_dist_orthogonalProjection_eq, dist_orthogonalProjection_eq_infDist, orthogonalProjection_mem, dist_orthogonalProjection_eq_zero_iff, exists_dist_eq_iff_exists_dist_orthogonalProjection_eq, Sphere.IsTangentAt.eq_orthogonalProjection, reflection_eq_iff_orthogonalProjection_eq, orthogonalProjection_orthogonalProjection, orthogonalProjection_vsub_mem_direction, vsub_orthogonalProjection_mem_direction, Sphere.IsTangent.isTangentAt, reflection_apply', oangle_self_orthogonalProjection, orthogonalProjection_linear, AffineSubspace.signedInfDist_def, angle_self_orthogonalProjection, orthogonalProjection_eq_self_iff, orthogonalProjection_vsub_mem_direction_orthogonal, eq_orthogonalProjection_of_eq_subspace, orthogonalProjection_apply, AffineSubspace.signedInfDist_apply_self, orthogonalProjection_vsub_orthogonalProjection, orthogonalProjection_mem_orthogonal, two_zsmul_oangle_orthogonalProjection_self, coe_orthogonalProjection_eq_iff_mem, dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, orthogonalProjection_eq_iff_mem, dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, dist_set_eq_iff_dist_orthogonalProjection_eq, orthogonalProjection_mem_subspace_eq_self
reflection 📖	CompOp	22 math math: reflection_orthogonal_vadd, reflection_symm, reflection_map, reflection_vadd_smul_vsub_orthogonalProjection, Affine.Triangle.dist_circumcenter_reflection_orthocenter, reflection_reflection, reflection_eq_self_iff, Affine.Triangle.dist_orthocenter_reflection_circumcenter, reflection_apply_of_mem, eq_or_eq_reflection_of_dist_eq, dist_reflection_eq_of_mem, dist_reflection, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, reflection_eq_iff_orthogonalProjection_eq, reflection_apply', reflection_involutive, reflection_subtype, eq_reflection_of_eq_subspace, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, reflection_mem_of_le_of_mem, reflection_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_orthogonalProjection_eq_iff_mem 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.orthogonal VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	orthogonalProjection_mem vsub_orthogonalProjection_mem_direction_orthogonal AffineSubspace.mem_mk' neg_mem_iff AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass neg_vsub_eq_vsub_rev inter_eq_singleton_orthogonalProjection
dist_eq_iff_dist_orthogonalProjection_eq 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Dist.dist PseudoMetricSpace.toDist DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	mul_self_inj_of_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instIsStrictOrderedRing dist_nonneg dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq AddRightCancelSemigroup.toIsRightCancelAdd
dist_orthogonalProjection_eq_dist_iff_eq_of_mem 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Dist.dist PseudoMetricSpace.toDist DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	dist_eq_zero mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass right_eq_add AddRightCancelSemigroup.toIsRightCancelAdd dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq dist_comm pow_two sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_nonneg
dist_orthogonalProjection_eq_infDist 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Metric.infDist SetLike.coe	—	le_antisymm Metric.infDist_eq_iInf le_ciInf le_of_sq_le_sq Real.instIsStrictOrderedRing dist_comm pow_two dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing dist_nonneg Metric.infDist_le_dist_of_mem orthogonalProjection_mem
dist_orthogonalProjection_eq_infNndist 📖	mathematical	—	NNDist.nndist PseudoMetricSpace.toNNDist MetricSpace.toPseudoMetricSpace AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Metric.infNndist SetLike.coe	—	dist_orthogonalProjection_eq_infDist
dist_orthogonalProjection_eq_zero_iff 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Real Real.instZero	—	dist_comm dist_eq_zero orthogonalProjection_eq_self_iff
dist_orthogonalProjection_ne_zero_of_notMem 📖	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	—	—	dist_orthogonalProjection_eq_zero_iff
dist_reflection 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection	—	reflection_reflection AffineIsometryEquiv.dist_map
dist_reflection_eq_of_mem 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Dist.dist PseudoMetricSpace.toDist DFunLike.coe AffineIsometryEquiv EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection	—	reflection_eq_self_iff AffineIsometryEquiv.dist_map
dist_set_eq_iff_dist_orthogonalProjection_eq 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike	Set.Pairwise Real Dist.dist PseudoMetricSpace.toDist SetLike.instMembership DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	dist_eq_iff_dist_orthogonalProjection_eq
dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Real Real.instMul Dist.dist PseudoMetricSpace.toDist Real.instAdd DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	dist_comm dist_eq_norm_vsub vsub_add_vsub_cancel norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero Submodule.inner_right_of_mem_orthogonal vsub_orthogonalProjection_mem_direction orthogonalProjection_vsub_mem_direction_orthogonal
dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.setLike Submodule.orthogonal AffineSubspace.direction	Real Real.instMul Dist.dist PseudoMetricSpace.toDist HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Real.instAdd Norm.norm NormedField.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAddCommGroup.toNorm	—	dist_eq_norm_vsub vsub_vadd_eq_vsub_sub vadd_vsub_assoc sub_smul add_comm add_sub_assoc norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero Submodule.inner_right_of_mem_orthogonal AffineSubspace.vsub_mem_direction Submodule.smul_mem norm_smul NormedSpace.toNormSMulClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
eq_orthogonalProjection_of_eq_subspace 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	—
eq_reflection_of_eq_subspace 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection	—	—
exists_dist_eq_iff_exists_dist_orthogonalProjection_eq 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike	Dist.dist PseudoMetricSpace.toDist SetLike.instMembership DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	dist_set_eq_iff_dist_orthogonalProjection_eq
inter_eq_singleton_orthogonalProjection 📖	mathematical	—	Set Set.instInter SetLike.coe AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace.instSetLike CommRing.toRing Field.toCommRing NormedField.toField AffineSubspace.mk' Submodule.orthogonal AffineSubspace.direction Set.instSingletonSet SetLike.instMembership DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl nonempty_subtype AffineSubspace.mk'_nonempty AffineSubspace.direction_mk' Submodule.isCompl_orthogonal_of_hasOrthogonalProjection Set.eq_singleton_iff_nonempty_unique_mem orthogonalProjection_mem orthogonalProjection_mem_orthogonal
orthogonalProjection_affineSpan_singleton 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instSingletonSet DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.Elem Unique.instInhabited Set.uniqueSingleton ContinuousAffineMap.instFunLike orthogonalProjection Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_direction_affineSpan_singleton SetLike.coe_mem AffineSubspace.mem_affineSpan_singleton
orthogonalProjection_apply 📖	mathematical	—	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace AffineSubspace.instSetLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection HVAdd.hVAdd DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid Submodule.normedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid ContinuousLinearMap.funLike Submodule.orthogonalProjection VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Classical.arbitrary	—	—
orthogonalProjection_apply' 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid ContinuousLinearMap.funLike Submodule.orthogonalProjection VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Classical.arbitrary	—	—
orthogonalProjection_apply_mem 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid ContinuousLinearMap.funLike Submodule.orthogonalProjection VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	orthogonalProjection_apply AffineSubspace.coe_vadd vadd_eq_vadd_iff_sub_eq_vsub Submodule.addSubgroupClass Submodule.coe_sub map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass vsub_sub_vsub_cancel_left Submodule.coe_orthogonalProjection_apply Submodule.starProjection_eq_self_iff AffineSubspace.vsub_mem_direction SetLike.coe_mem
orthogonalProjection_congr 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Submodule.HasOrthogonalProjection	—	—
orthogonalProjection_contLinear 📖	mathematical	—	ContinuousAffineMap.contLinear Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace AffineSubspace.instSetLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace instIsTopologicalAddTorsor_1 AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection orthogonalProjection Submodule.orthogonalProjection	—	instIsTopologicalAddTorsor_1 AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection
orthogonalProjection_eq_iff_mem 📖	mathematical	—	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace AffineSubspace.instSetLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.orthogonal VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	coe_orthogonalProjection_eq_iff_mem
orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem 📖	mathematical	—	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace AffineSubspace.instSetLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.orthogonal VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	orthogonalProjection_eq_iff_mem Submodule.add_mem_iff_left vsub_orthogonalProjection_mem_direction_orthogonal vsub_add_vsub_cancel
orthogonalProjection_eq_self_iff 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	orthogonalProjection_mem AffineSubspace.self_mem_mk' inter_eq_singleton_orthogonalProjection
orthogonalProjection_linear 📖	mathematical	—	AffineMap.linear Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module AffineSubspace.toAddTorsor ContinuousAffineMap.toAffineMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instTopologicalSpaceSubtype orthogonalProjection ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.addCommMonoid Submodule.orthogonalProjection	—	—
orthogonalProjection_map 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.map SeminormedAddCommGroup.toAddCommGroup AffineIsometry.toAffineMap DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor AffineSubspace.nonempty_map ContinuousAffineMap.instFunLike orthogonalProjection AffineIsometry AffineIsometry.instFunLike	—	AffineSubspace.nonempty_map coe_orthogonalProjection_eq_iff_mem RingHomSurjective.ids AffineIsometry.coe_toAffineMap AffineSubspace.map_direction Submodule.map.congr_simp AffineIsometry.linear_eq_linearIsometry AffineMap.linearMap_vsub Submodule.mem_orthogonal Submodule.mem_map LinearIsometry.coe_toLinearMap LinearIsometry.inner_map_map Submodule.inner_right_of_mem_orthogonal vsub_orthogonalProjection_mem_direction_orthogonal
orthogonalProjection_mem 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	—
orthogonalProjection_mem_orthogonal 📖	mathematical	—	AffineSubspace CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.mk' Submodule.orthogonal AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	AffineSubspace.mem_mk' orthogonalProjection_apply AffineSubspace.coe_vadd vadd_vsub_eq_sub_vsub Submodule.neg_mem_iff neg_sub Submodule.sub_starProjection_mem_orthogonal
orthogonalProjection_mem_subspace_eq_self 📖	mathematical	—	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace AffineSubspace.instSetLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	orthogonalProjection_eq_self_iff
orthogonalProjection_orthogonalProjection 📖	mathematical	—	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace AffineSubspace.instSetLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	orthogonalProjection_mem_subspace_eq_self
orthogonalProjection_orthogonalProjection_of_le 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem SetLike.le_def instIsConcreteLE Submodule.orthogonal_le AffineSubspace.direction_le orthogonalProjection_vsub_mem_direction_orthogonal
orthogonalProjection_subtype 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor DFunLike.coe ContinuousAffineMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection AffineSubspace.map AffineSubspace.subtype AffineSubspace.nonempty_map	—	AffineSubspace.nonempty_map IsScalarTower.left AffineSubspace.subtypeₐᵢ_toAffineMap orthogonalProjection_congr orthogonalProjection_map
orthogonalProjection_sup_of_orthogonalProjection_eq 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AffineSubspace.instCompleteLattice AffineSubspace.nonempty_sup_right	—	AffineSubspace.nonempty_sup_right coe_orthogonalProjection_eq_iff_mem SetLike.le_def instIsConcreteLE le_sup_left orthogonalProjection_mem AffineSubspace.direction_sup_eq_sup_direction Submodule.inf_orthogonal vsub_orthogonalProjection_mem_direction_orthogonal
orthogonalProjection_vadd_eq_self 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.setLike Submodule.orthogonal AffineSubspace.direction	DFunLike.coe ContinuousAffineMap Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	vsub_orthogonalProjection_mem_direction_orthogonal eq_of_vsub_eq_zero Submodule.disjoint_def Submodule.orthogonal_disjoint Submodule.add_mem_iff_right vadd_vsub_assoc
orthogonalProjection_vadd_smul_vsub_orthogonalProjection 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	DFunLike.coe ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	orthogonalProjection_vadd_eq_self Submodule.smul_mem vsub_orthogonalProjection_mem_direction_orthogonal
orthogonalProjection_vsub_mem_direction 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Submodule.addCommGroup AffineSubspace.toAddTorsor DFunLike.coe ContinuousAffineMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype ContinuousAffineMap.instFunLike orthogonalProjection	—	—
orthogonalProjection_vsub_mem_direction_orthogonal 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AffineSubspace AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	AffineSubspace.mem_mk' orthogonalProjection_mem_orthogonal
orthogonalProjection_vsub_orthogonalProjection 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike Submodule.orthogonalProjection VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AffineSubspace AffineSubspace.instSetLike ContinuousAffineMap Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection Submodule.zero	—	vsub_orthogonalProjection_mem_direction_orthogonal
reflection_apply 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedSpace.toModule LinearIsometryEquiv.instEquivLike Submodule.reflection AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AffineSubspace SetLike.instMembership AffineSubspace.instSetLike Classical.arbitrary	—	—
reflection_apply' 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule SetLike.instMembership AffineSubspace.instSetLike ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	RingHomInvPair.ids reflection_apply orthogonalProjection_apply' Submodule.coe_orthogonalProjection_apply Submodule.reflection_apply Nat.instAtLeastTwoHAddOfNat two_smul sub_eq_add_neg neg_vsub_eq_vsub_rev add_assoc add_comm AddSemigroupAction.add_vadd vadd_vsub_assoc
reflection_apply_of_mem 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	DFunLike.coe AffineIsometryEquiv EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearIsometryEquiv.instEquivLike Submodule.reflection AffineSubspace.direction VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	RingHomInvPair.ids reflection_apply vadd_eq_vadd_iff_sub_eq_vsub map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass vsub_sub_vsub_cancel_left Submodule.reflection_eq_self_iff AffineSubspace.vsub_mem_direction SetLike.coe_mem
reflection_eq_iff_orthogonalProjection_eq 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	reflection_apply' Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero two_smul vsub_sub_vsub_cancel_right add_sub_assoc add_comm vadd_vsub_assoc vsub_vadd_eq_vsub_sub vsub_eq_zero_iff_eq
reflection_eq_self_iff 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike	—	RingHomInvPair.ids reflection_apply eq_vadd_iff_vsub_eq Submodule.reflection_eq_self_iff AffineSubspace.mem_direction_iff_eq_vsub_right SetLike.coe_mem
reflection_involutive 📖	mathematical	—	Function.Involutive DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection	—	reflection_reflection
reflection_map 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection AffineSubspace.map NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor NormedAddCommGroup.toAddCommGroup AffineIsometry.toAffineMap AffineSubspace.nonempty_map AffineIsometry AffineIsometry.instFunLike	—	AffineSubspace.nonempty_map reflection_apply' orthogonalProjection_map AffineIsometry.map_vadd AffineIsometry.map_vsub
reflection_mem_of_le_of_mem 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder SetLike.instMembership AffineSubspace.instSetLike	DFunLike.coe AffineIsometryEquiv EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection	—	reflection_apply' orthogonalProjection_mem AffineSubspace.vadd_mem_of_mem_direction AffineSubspace.vsub_mem_direction
reflection_orthogonal_vadd 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.setLike Submodule.orthogonal AffineSubspace.direction	DFunLike.coe AffineIsometryEquiv EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	reflection_apply' orthogonalProjection_vadd_eq_self vsub_vadd_eq_vsub_sub vsub_self zero_sub
reflection_reflection 📖	mathematical	—	DFunLike.coe AffineIsometryEquiv DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection	—	RingHomInvPair.ids LinearIsometryEquiv.coe_toAffineIsometryEquiv vadd_vsub Submodule.reflection_reflection vsub_vadd
reflection_subtype 📖	mathematical	—	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe AffineIsometryEquiv Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection AffineSubspace.map Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor AffineSubspace.subtype AffineSubspace.nonempty_map	—	AffineSubspace.nonempty_map reflection_apply' orthogonalProjection_subtype
reflection_symm 📖	mathematical	—	AffineIsometryEquiv.symm DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MetricSpace.toPseudoMetricSpace reflection	—	AffineIsometryEquiv.ext AffineIsometryEquiv.injective AffineIsometryEquiv.apply_symm_apply reflection_reflection
reflection_vadd_smul_vsub_orthogonalProjection 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	DFunLike.coe AffineIsometryEquiv EquivLike.toFunLike AffineIsometryEquiv.instEquivLike reflection HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	reflection_orthogonal_vadd Submodule.smul_mem vsub_orthogonalProjection_mem_direction_orthogonal
vsub_orthogonalProjection_mem_direction 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Submodule.addCommGroup AffineSubspace.toAddTorsor DFunLike.coe ContinuousAffineMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype ContinuousAffineMap.instFunLike orthogonalProjection	—	—
vsub_orthogonalProjection_mem_direction_orthogonal 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal AffineSubspace.direction NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup AffineSubspace AffineSubspace.instSetLike DFunLike.coe ContinuousAffineMap Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module instTopologicalSpaceSubtype AffineSubspace.toAddTorsor ContinuousAffineMap.instFunLike orthogonalProjection	—	AffineSubspace.vsub_mem_direction AffineSubspace.self_mem_mk' orthogonalProjection_mem_orthogonal AffineSubspace.direction_mk'

---

← Back to Index