SecondInter

📁 Source: Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean

Statistics

Metric	Count
Definitions secondInter	1
Theorems coe_secondInter, eq_or_eq_secondInter_iff_mem_of_mem_affineSpan_pair, eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem, sOppSide_faceOpposite_secondInter_of_mem_interior, sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite, sbtw_secondInter, secondInter_collinear, secondInter_dist, secondInter_eq_lineMap, secondInter_eq_self_iff, secondInter_map, secondInter_mem, secondInter_neg, secondInter_secondInter, secondInter_smul, secondInter_vsub_mem_affineSpan, secondInter_zero, wbtw_secondInter	18
Total	19

EuclideanGeometry.Sphere

Definitions

Name	Category	Theorems
secondInter 📖	CompOp	18 math math: secondInter_neg, wbtw_secondInter, secondInter_mem, secondInter_dist, eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem, secondInter_collinear, coe_secondInter, sbtw_secondInter, secondInter_smul, sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite, sOppSide_faceOpposite_secondInter_of_mem_interior, secondInter_secondInter, secondInter_vsub_mem_affineSpan, secondInter_zero, secondInter_eq_lineMap, secondInter_map, secondInter_eq_self_iff, eq_or_eq_secondInter_iff_mem_of_mem_affineSpan_pair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_secondInter 📖	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 secondInter Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.normedAddCommGroup Submodule.innerProductSpace Subtype.metricSpace AffineSubspace.toNormedAddTorsor center radius	—	—
eq_or_eq_secondInter_iff_mem_of_mem_affineSpan_pair 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere 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 Set.instInsert Set.instSingletonSet	secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem AffineSubspace.eq_iff_direction_eq_of_mem AffineSubspace.self_mem_mk' left_mem_affineSpan_pair AffineSubspace.direction_mk' direction_affineSpan vectorSpan_pair_rev
eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.mk' Submodule.span Real.semiring AddCommGroup.toAddCommMonoid Set Set.instSingletonSet	secondInter	—	secondInter_mem Submodule.mem_span_singleton AffineSubspace.mem_mk' smul_zero zero_vadd secondInter_zero secondInter.eq_1 Nat.instAtLeastTwoHAddOfNat EuclideanGeometry.dist_smul_vadd_eq_dist EuclideanGeometry.mem_sphere zero_smul neg_mul inner_self_eq_norm_sq_to_K eq_vadd_iff_vsub_eq
sOppSide_faceOpposite_secondInter_of_mem_interior 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.instLE Dist.dist PseudoMetricSpace.toDist center radius Set Set.instMembership Affine.Simplex.interior Real.partialOrder	AffineSubspace.SOppSide Real.commRing Real.instIsStrictOrderedRing affineSpan Set.range Affine.Simplex.faceOpposite Nat.AtLeastTwo.toNeZero secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Real.instIsStrictOrderedRing Nat.AtLeastTwo.toNeZero PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AffineMap.lineMap_vsub_left sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite Finset.affineCombination_affineCombinationSingleWeights Finset.mem_univ Finset.affineCombination_vsub Finset.weightedVSub_vadd_affineCombination Affine.Simplex.affineCombination_mem_interior_face_iff_pos Nat.AtLeastTwo.neZero_sub_one Finset.sum_congr Finset.sum_add_distrib Finset.sum_sub_distrib Finset.sum_affineCombinationSingleWeights sub_self MulZeroClass.mul_zero zero_add Finset.affineCombinationSingleWeights_apply_self Finset.affineCombinationSingleWeights_apply_of_ne sub_zero add_zero secondInter_smul LT.lt.ne'
sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Affine.Simplex.points Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.instLE Dist.dist PseudoMetricSpace.toDist center radius Set Set.instMembership Affine.Simplex.interior Real.partialOrder Affine.Simplex.faceOpposite	AffineSubspace.SOppSide Real.commRing Real.instIsStrictOrderedRing affineSpan Set.range secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Sbtw.sOppSide_of_notMem_of_mem Real.instIsStrictOrderedRing sbtw_secondInter Affine.Simplex.dist_lt_of_mem_interior_of_strictConvexSpace UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace Affine.Simplex.range_faceOpposite_points Real.instNontrivial Set.mem_of_mem_of_subset HasSubset.Subset.trans Set.instIsTransSubset Affine.Simplex.interior_subset_closedInterior Affine.Simplex.closedInterior_subset_affineSpan
sbtw_secondInter 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Real Real.instLT Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius	Sbtw Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	wbtw_secondInter LT.lt.le EuclideanGeometry.mem_sphere lt_irrefl secondInter_mem
secondInter_collinear 📖	mathematical	—	Collinear Real Real.instDivisionRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Set Set.instInsert Set.instSingletonSet secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Set.pair_comm Set.insert_comm collinear_insert_iff_of_mem_affineSpan secondInter_vsub_mem_affineSpan collinear_pair
secondInter_dist 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace secondInter center	—	secondInter.eq_1 inner_zero_left MulZeroClass.mul_zero inner_self_eq_norm_sq_to_K norm_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat div_zero smul_zero zero_vadd EuclideanGeometry.dist_smul_vadd_eq_dist
secondInter_eq_lineMap 📖	mathematical	—	secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace DFunLike.coe AffineMap Real Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike AffineMap.instFunLike AffineMap.lineMap DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner center	—	—
secondInter_eq_self_iff 📖	mathematical	—	secondInter Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace center Real.instZero	—	inner_zero_left Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass inner_self_eq_zero div_eq_zero_iff smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero vsub_self eq_vadd_iff_vsub_eq secondInter.eq_1 MulZeroClass.mul_zero zero_div zero_smul zero_vadd
secondInter_map 📖	mathematical	—	secondInter DFunLike.coe AffineIsometry Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike MetricSpace.toPseudoMetricSpace AffineIsometry.instFunLike center radius LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule LinearIsometry.instFunLike AffineIsometry.linearIsometry	—	LinearIsometry.inner_map_map neg_mul inner_self_eq_norm_sq_to_K LinearIsometry.norm_map AffineIsometry.map_vadd map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass LinearIsometry.instSemilinearIsometryClass
secondInter_mem 📖	mathematical	—	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere secondInter	—	secondInter_dist
secondInter_neg 📖	mathematical	—	secondInter NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg_one_smul secondInter_smul NeZero.charZero_one RCLike.charZero_rclike
secondInter_secondInter 📖	mathematical	—	secondInter	—	secondInter_zero inner_self_ne_zero vadd_vsub_assoc inner_add_right inner_smul_right div_mul_cancel₀ vadd_vadd vsub_eq_zero_iff_eq vadd_vsub add_smul add_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero zero_div zero_smul
secondInter_smul 📖	mathematical	—	secondInter Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	real_inner_smul_left inner_smul_right smul_smul div_mul_eq_div_div mul_comm mul_div_assoc mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass mul_assoc
secondInter_vsub_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 Set.instInsert Set.instSingletonSet secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	smul_vsub_vadd_mem_affineSpan_pair
secondInter_zero 📖	mathematical	—	secondInter NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	inner_zero_left MulZeroClass.mul_zero inner_self_eq_norm_sq_to_K norm_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat div_zero smul_zero zero_vadd
wbtw_secondInter 📖	mathematical	EuclideanGeometry.Sphere EuclideanGeometry.instMembershipSphere Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace center radius	Wbtw Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor secondInter VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	vsub_self secondInter_zero Real.instIsOrderedRing EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius secondInter_collinear secondInter_mem LT.lt.ne EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius neg_eq_zero neg_vsub_eq_vsub_rev inner_neg_left neg_neg secondInter_eq_self_iff

---

← Back to Index