📁 Source: Mathlib/Geometry/Euclidean/Angle/Bisector.lean
dist_orthogonalProjection_eq_iff_angle_eq
dist_orthogonalProjection_eq_iff_oangle_eq
dist_orthogonalProjection_eq_of_oangle_eq
dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq
dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq
dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq
oangle_eq_of_dist_orthogonalProjection_eq
two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_eq
AffineSubspace
Real
Real.instRing
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
Real.normedField
NormedAddCommGroup.toSeminormedAddCommGroup
InnerProductSpace.toNormedSpace
Real.instRCLike
NormedAddTorsor.toAddTorsor
MetricSpace.toPseudoMetricSpace
SetLike.instMembership
AffineSubspace.instSetLike
Dist.dist
PseudoMetricSpace.toDist
NormedRing.toRing
NormedCommRing.toNormedRing
NormedField.toNormedCommRing
DenselyNormedField.toNormedField
RCLike.toDenselyNormedField
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
angle
angle_comm
angle_eq_arcsin_of_angle_eq_pi_div_two
angle_self_orthogonalProjection
Iff.not
orthogonalProjection_eq_self_iff
dist_pos
div_left_inj'
LT.lt.ne'
le_trans
Mathlib.Meta.NormNum.isInt_le_true
Real.instIsOrderedRing
Mathlib.Meta.NormNum.isInt_neg
Mathlib.Meta.NormNum.IsNat.to_isInt
Mathlib.Meta.NormNum.isNat_ofNat
Nat.cast_one
Nat.cast_zero
Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos
PosMulReflectLE.toPosMulReflectLT
PosMulStrictMono.toPosMulReflectLE
IsStrictOrderedRing.toPosMulStrictMono
Real.instIsStrictOrderedRing
dist_nonneg
div_le_one
dist_orthogonalProjection_eq_infDist
Metric.infDist_le_dist_of_mem
SetLike.mem_coe
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.finiteDimensional_submodule
Real.instDivisionRing
FiniteDimensional.of_fact_finrank_eq_two
oangle
angle_eq_iff_oangle_eq_or_wbtw
Real.Angle
SubNegMonoid.toZSMul
AddGroup.toSubNegMonoid
NormedAddGroup.toAddGroup
NormedAddCommGroup.toNormedAddGroup
Real.instNormedAddCommGroupAngle
oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two
AffineIndependent
Matrix.vecCons
Matrix.vecEmpty
affineSpan
Set
Set.instInsert
Set.instSingletonSet
instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem
Set.instNonemptyElemInsert
finiteDimensional_direction_affineSpan_insert_set
finiteDimensional_direction_affineSpan_singleton
AffineIndependent.injective
Real.instNontrivial
left_mem_affineSpan_pair
Collinear.two_zsmul_oangle_eq_left
collinear_insert_of_mem_affineSpan_pair
orthogonalProjection_mem
Collinear.two_zsmul_oangle_eq_right
dist_orthogonalProjection_eq_dist_iff_eq_of_mem
Collinear.mem_affineSpan_of_mem_of_ne
SetLike.le_def
instIsConcreteLE
affineSpan_pair_le_of_mem_of_mem
orthogonalProjection_orthogonalProjection_of_le
inf_le_left
inf_le_right
Wbtw.collinear
Set.pair_comm
AffineSubspace.nonempty_sup_right
AffineSubspace.finiteDimensional_sup
orthogonalProjection_sup_of_orthogonalProjection_eq
Set.image_congr
Set.image_insert_eq
Set.image_singleton
AffineIndependent.inf_affineSpan_eq_affineSpan_inter
AffineSubspace.span_union
Set.union_insert
Set.union_singleton
Set.insert_eq_of_mem
Matrix.range_cons
Matrix.range_empty
Set.union_empty
AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one
Fintype.card_congr'
zero_add
Fintype.card_fin
Fact.out
AffineSubspace.mem_top
oangle.congr_simp
oangle_self_right
smul_zero
oangle_self_left
---
← Back to Index