Altitude

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

Statistics

Metric	Count
Definitions altitude, altitudeFoot, evalHeight, height	4
Theorems abs_inner_vsub_altitudeFoot_div_lt_one, abs_inner_vsub_altitudeFoot_lt_mul, affineSpan_pair_altitudeFoot_eq_altitude, affineSpan_pair_eq_altitude_iff, altitudeFoot_map, altitudeFoot_mem_affineSpan, altitudeFoot_mem_affineSpan_faceOpposite, altitudeFoot_mem_affineSpan_image_compl, altitudeFoot_mem_altitude, altitudeFoot_reindex, altitudeFoot_restrict, altitude_def, altitude_map, altitude_reindex, altitude_restrict_eq_comap_subtype, direction_altitude, finiteDimensional_direction_altitude, finrank_direction_altitude, height_map, height_pos, height_reindex, height_restrict, inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero, inner_vsub_vsub_altitudeFoot_eq_height_sq, map_altitude_restrict, mem_altitude, ne_altitudeFoot, neg_mul_lt_inner_vsub_altitudeFoot, neg_one_lt_inner_vsub_altitudeFoot_div, vectorSpan_isOrtho_altitude_direction	30
Total	34

Affine.Simplex

Definitions

Name	Category	Theorems
altitude 📖	CompOp	17 math math: finiteDimensional_direction_altitude, Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan, affineSpan_pair_altitudeFoot_eq_altitude, finrank_direction_altitude, altitude_restrict_eq_comap_subtype, vectorSpan_isOrtho_altitude_direction, map_altitude_restrict, altitudeFoot_mem_altitude, Affine.Triangle.affineSpan_orthocenter_point_le_altitude, altitude_reindex, Affine.Triangle.orthocenter_mem_altitude, altitude_map, mem_altitude, Affine.Triangle.altitude_eq_mongePlane, affineSpan_pair_eq_altitude_iff, direction_altitude, altitude_def
altitudeFoot 📖	CompOp	17 math math: altitudeFoot_restrict, neg_mul_lt_inner_vsub_altitudeFoot, inv_height_eq_sum_mul_inv_dist, affineSpan_pair_altitudeFoot_eq_altitude, abs_inner_vsub_altitudeFoot_div_lt_one, altitudeFoot_mem_affineSpan_image_compl, abs_inner_vsub_altitudeFoot_lt_mul, altitudeFoot_map, Affine.Triangle.altitudeFoot_mem_ninePointCircle, altitudeFoot_mem_affineSpan, altitudeFoot_reindex, altitudeFoot_mem_altitude, inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero, sum_inv_height_sq_smul_vsub_eq_zero, neg_one_lt_inner_vsub_altitudeFoot_div, altitudeFoot_mem_affineSpan_faceOpposite, inner_vsub_vsub_altitudeFoot_eq_height_sq
evalHeight 📖	CompOp	—
height 📖	CompOp	13 math math: neg_mul_lt_inner_vsub_altitudeFoot, inv_height_eq_sum_mul_inv_dist, abs_inner_vsub_altitudeFoot_div_lt_one, inv_height_lt_sum_inv_height, abs_inner_vsub_altitudeFoot_lt_mul, height_map, excenterWeightsUnnorm_empty_apply, height_restrict, height_pos, sum_inv_height_sq_smul_vsub_eq_zero, neg_one_lt_inner_vsub_altitudeFoot_div, height_reindex, inner_vsub_vsub_altitudeFoot_eq_height_sq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_inner_vsub_altitudeFoot_div_lt_one 📖	mathematical	—	Real Real.instLT abs Real.lattice Real.instAddGroup DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace altitudeFoot Nat.AtLeastTwo.toNeZero Real.instMul height Real.instOne	—	Nat.AtLeastTwo.toNeZero abs_div Real.instIsStrictOrderedRing div_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono abs_mul Real.instIsOrderedRing abs_dist abs_eq_self Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono dist_nonneg abs_inner_vsub_altitudeFoot_lt_mul
abs_inner_vsub_altitudeFoot_lt_mul 📖	mathematical	—	Real Real.instLT abs Real.lattice Real.instAddGroup Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace altitudeFoot Nat.AtLeastTwo.toNeZero Real.instMul height	—	lt_of_le_of_ne Nat.AtLeastTwo.toNeZero dist_eq_norm_vsub abs_real_inner_le_norm Real.norm_eq_abs norm_inner_eq_norm_iff Submodule.mem_bot Submodule.inf_orthogonal_eq_bot vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan mem_affineSpan Set.mem_range_self SetLike.le_def instIsConcreteLE affineSpan_mono range_faceOpposite_points Set.preimage_range SetLike.mem_coe Fin.exists_ne_and_ne_of_two_lt lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_add Nat.cast_one Nat.AtLeastTwo.one_lt Set.mem_image_of_mem Set.inter_singleton_eq_empty Set.compl_empty AffineSubspace.vectorSpan_union_of_mem_of_mem Submodule.inf_orthogonal Submodule.mem_inf direction_affineSpan Submodule.smul_mem EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal
affineSpan_pair_altitudeFoot_eq_altitude 📖	mathematical	—	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert altitudeFoot Set.instSingletonSet points altitude	—	affineSpan_pair_eq_altitude_iff ne_altitudeFoot altitudeFoot_mem_affineSpan altitudeFoot.eq_1 instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange orthogonalProjectionSpan.eq_1 range_faceOpposite_points EuclideanGeometry.orthogonalProjection_congr EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
affineSpan_pair_eq_altitude_iff 📖	mathematical	—	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet points altitude AffineSubspace SetLike.instMembership AffineSubspace.instSetLike Set.range Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.setLike Submodule.orthogonal AffineSubspace.direction Set.image Compl.compl Set.instCompl VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	AffineSubspace.eq_iff_direction_eq_of_mem mem_affineSpan Set.mem_insert_of_mem Set.mem_singleton mem_altitude AffineSubspace.vsub_right_mem_direction_iff_mem Set.mem_range_self direction_affineSpan vectorSpan_singleton Set.pair_eq_singleton finrank_bot Real.instNontrivial finrank_direction_altitude Submodule.mem_inf inf_comm direction_altitude vsub_mem_vectorSpan Set.mem_insert vectorSpan_eq_span_vsub_set_left_ne Set.insert_diff_of_mem Set.diff_singleton_eq_self Set.mem_singleton_iff Set.image_singleton Submodule.eq_of_le_of_finrank_eq finiteDimensional_direction_altitude Submodule.span_le finrank_span_set_eq_card commRing_strongRankCondition LinearIndepOn.singleton Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Set.toFinset_singleton Finset.card_singleton
altitudeFoot_map 📖	mathematical	—	altitudeFoot map Real Real.instRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineIsometry.toAffineMap AffineIsometry.injective DFunLike.coe AffineIsometry AffineIsometry.instFunLike	—	AffineIsometry.injective instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.coe_toAffineMap
altitudeFoot_mem_affineSpan 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points altitudeFoot	—	SetLike.le_def instIsConcreteLE affineSpan_mono range_faceOpposite_points Set.preimage_range altitudeFoot_mem_affineSpan_faceOpposite
altitudeFoot_mem_affineSpan_faceOpposite 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite altitudeFoot	—	EuclideanGeometry.orthogonalProjection_mem
altitudeFoot_mem_affineSpan_image_compl 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.image points Compl.compl Set Set.instCompl Set.instSingletonSet altitudeFoot	—	range_faceOpposite_points EuclideanGeometry.orthogonalProjection_mem
altitudeFoot_mem_altitude 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike altitude altitudeFoot	—	affineSpan_pair_altitudeFoot_eq_altitude left_mem_affineSpan_pair
altitudeFoot_reindex 📖	mathematical	—	altitudeFoot reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	orthogonalProjectionSpan_congr range_faceOpposite_reindex
altitudeFoot_restrict 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	SetLike.instMembership AffineSubspace.instSetLike altitudeFoot 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	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.injective altitudeFoot_map
altitude_def 📖	mathematical	—	altitude AffineSubspace Real CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AffineSubspace.instCompleteLattice AffineSubspace.mk' points Real.instRing NormedAddCommGroup.toAddCommGroup Real.normedField Submodule.orthogonal AffineSubspace.direction affineSpan Set.image Compl.compl Set Set.instCompl Set.instSingletonSet Set.range	—	—
altitude_map 📖	mathematical	—	altitude map Real Real.instRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineIsometry.toAffineMap AffineIsometry.injective AffineSubspace.map NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing	—	AffineIsometry.injective AffineSubspace.eq_iff_direction_eq_of_mem mem_altitude AffineSubspace.mem_map_of_mem LinearIsometry.injective RingHomSurjective.ids AffineSubspace.map_direction direction_altitude Submodule.map_inf AffineIsometry.linear_eq_linearIsometry Submodule.map_orthogonal map_points Set.range_comp Set.image_comp AffineMap.map_vectorSpan inf_assoc Submodule.map_top top_inf_eq
altitude_reindex 📖	mathematical	—	altitude reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineSubspace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	AffineSubspace.ext Set.image_congr Set.image_comp Equiv.image_compl Set.image_singleton reindex_range_points
altitude_restrict_eq_comap_subtype 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	altitude Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike 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 AffineSubspace.comap AffineSubspace.subtype	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange map_altitude_restrict AffineSubspace.comap_map_eq_of_injective AffineSubspace.subtype_injective
direction_altitude 📖	mathematical	—	AffineSubspace.direction Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace altitude Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.instMin Submodule.orthogonal vectorSpan SeminormedAddCommGroup.toAddCommGroup Set.image points Compl.compl Set Set.instCompl Set.instSingletonSet Set.range	—	altitude_def AffineSubspace.direction_inf_of_mem AffineSubspace.self_mem_mk' mem_affineSpan Set.mem_range_self AffineSubspace.direction_mk' direction_affineSpan
finiteDimensional_direction_altitude 📖	mathematical	—	FiniteDimensional Real Submodule Ring.toSemiring Real.instRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace altitude Real.instDivisionRing Submodule.addCommGroup SeminormedAddCommGroup.toAddCommGroup Submodule.module	—	direction_altitude Submodule.finiteDimensional_inf_right finiteDimensional_vectorSpan_range Finite.of_fintype
finrank_direction_altitude 📖	mathematical	—	Module.finrank Real Submodule Ring.toSemiring Real.instRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace altitude Real.semiring Submodule.addCommMonoid Submodule.module	—	direction_altitude Submodule.finrank_add_inf_finrank_orthogonal finiteDimensional_vectorSpan_range Finite.of_fintype vectorSpan_mono Set.image_subset_range Finset.card_compl Finset.card_singleton Fintype.card_fin add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid add_left_cancel trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv AffineIndependent.finrank_vectorSpan independent Finset.coe_singleton Finset.coe_compl Finset.coe_image AffineIndependent.finrank_vectorSpan_image_finset
height_map 📖	mathematical	—	height map Real Real.instRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineIsometry.toAffineMap AffineIsometry.injective	—	AffineIsometry.injective AffineIsometry.coe_toAffineMap altitudeFoot_map AffineIsometry.dist_map
height_pos 📖	mathematical	—	Real Real.instLT Real.instZero height	—	—
height_reindex 📖	mathematical	—	height reindex Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	altitudeFoot_reindex
height_restrict 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	height Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike 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	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.injective height_map
inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace altitudeFoot Real.instZero	—	Submodule.inner_right_of_mem_orthogonal vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan mem_affineSpan_image_iff Real.instNontrivial altitudeFoot_mem_affineSpan_image_compl direction_affineSpan range_faceOpposite_points EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal
inner_vsub_vsub_altitudeFoot_eq_height_sq 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace altitudeFoot Monoid.toNatPow Real.instMonoid height	—	inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero height.eq_1 inner_vsub_vsub_left_eq_dist_sq_right_iff inner_vsub_left_eq_zero_symm
map_altitude_restrict 📖	mathematical	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	AffineSubspace.map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion AffineSubspace.subtype altitude Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineIsometry.injective altitude_map
mem_altitude 📖	mathematical	—	AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike altitude points	—	AffineSubspace.mem_inf_iff AffineSubspace.self_mem_mk' mem_affineSpan Set.mem_range_self
ne_altitudeFoot 📖	—	—	—	—	range_faceOpposite_points Real.instNontrivial EuclideanGeometry.orthogonalProjection_eq_self_iff instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange orthogonalProjectionSpan.eq_1 altitudeFoot.eq_1
neg_mul_lt_inner_vsub_altitudeFoot 📖	mathematical	—	Real Real.instLT Real.instNeg Real.instMul height Nat.AtLeastTwo.toNeZero Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace altitudeFoot	—	Nat.AtLeastTwo.toNeZero eq_or_ne real_inner_self_eq_norm_sq lt_of_lt_of_le neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing height_pos Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul neg_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add lt_of_abs_lt abs_neg abs_inner_vsub_altitudeFoot_lt_mul
neg_one_lt_inner_vsub_altitudeFoot_div 📖	mathematical	—	Real Real.instLT Real.instNeg Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace points Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace altitudeFoot Nat.AtLeastTwo.toNeZero Real.instMul height	—	Nat.AtLeastTwo.toNeZero neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add neg_div' div_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing neg_mul_lt_inner_vsub_altitudeFoot
vectorSpan_isOrtho_altitude_direction 📖	mathematical	—	Submodule.IsOrtho Real Real.instRCLike vectorSpan Real.instRing SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set.image points NormedAddCommGroup.toAddCommGroup Real.normedField Compl.compl Set Set.instCompl Set.instSingletonSet AffineSubspace.direction altitude	—	direction_altitude Submodule.IsOrtho.mono_right inf_le_left Submodule.isOrtho_orthogonal_right

---

← Back to Index