Defs

📁 Source: Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

Statistics

Metric	Count
Definitions carrier, direction, directionOfNonempty, gi, instCompleteLattice, instInhabited, instPartialOrder, instSetLike, mk', toAffineSubspace, affineSpan, spanPoints, vectorSpan, «termLine[_,_,_]»	14
Theorems affineSpan_coe, affineSpan_eq_sInf, affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, bot_coe, bot_ne_top, card_pos_of_affineSpan_eq_top, coe_direction_eq_vsub_set, coe_direction_eq_vsub_set_left, coe_direction_eq_vsub_set_right, coe_eq_bot_iff, coe_eq_univ_iff, coe_iInf, coe_inf, coe_injective, coe_sInf, directionOfNonempty_eq_direction, direction_bot, direction_eq_top_iff_of_nonempty, direction_eq_vectorSpan, direction_iInf, direction_iInf_of_mem, direction_iInf_of_mem_iInf, direction_inf, direction_inf_of_mem, direction_inf_of_mem_inf, direction_le, direction_mk', direction_sInf, direction_sInf_of_mem, direction_sInf_of_mem_sInf, direction_top, eq_bot_or_nonempty, eq_iff_direction_eq_of_mem, eq_of_direction_eq_of_nonempty_of_le, exists_of_lt, ext, ext_iff, ext_of_direction_eq, inf_coe, instIsSimpleOrderOfSubsingleton, instNonemptySubtypeMemMk', instNonemptySubtypeMemTop, instNontrivial, inter_eq_singleton_of_nonempty_of_isCompl, inter_nonempty_of_nonempty_of_sup_direction_eq_top, isEmpty_bot, le_def, le_def', lt_def, lt_iff_le_and_exists, mem_coe, mem_direction_iff_eq_vsub, mem_direction_iff_eq_vsub_left, mem_direction_iff_eq_vsub_right, mem_iInf_iff, mem_inf_iff, mem_mk', mem_sInf_iff, mem_top, mk'_eq, mk'_nonempty, mk'_top, nonempty_iff_ne_bot, nonempty_of_affineSpan_eq_top, nonempty_sup_left, nonempty_sup_right, notMem_bot, not_le_iff_exists, self_mem_mk', smul_vsub_vadd_mem, spanPoints_subset_coe_of_subset_coe, span_empty, span_iUnion, span_union, span_univ, sup_direction_le, sup_direction_lt_of_nonempty_of_inter_empty, top_coe, vadd_mem_iff_mem_direction, vadd_mem_iff_mem_of_mem_direction, vadd_mem_mk', vadd_mem_of_mem_direction, vectorSpan_eq_top_of_affineSpan_eq_top, vsub_mem_direction, affineSpan, mem_toAffineSubspace, toAffineSubspace_direction, affineSpan_eq_bot, affineSpan_eq_top_iff_nonempty_of_subsingleton, affineSpan_induction, affineSpan_induction', affineSpan_insert_affineSpan, affineSpan_insert_eq_affineSpan, affineSpan_insert_zero, affineSpan_le, affineSpan_le_of_subset_coe, affineSpan_le_toAffineSubspace_span, affineSpan_mono, affineSpan_nonempty, affineSpan_pair_le_of_left_mem, affineSpan_pair_le_of_mem_of_mem, affineSpan_pair_le_of_right_mem, affineSpan_subset_span, bot_lt_affineSpan, coe_affineSpan, direction_affineSpan, instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem, left_mem_affineSpan_pair, mem_affineSpan, mem_affineSpan_iff_exists, mem_spanPoints, right_mem_affineSpan_pair, smul_vsub_mem_vectorSpan_pair, smul_vsub_rev_mem_vectorSpan_pair, spanPoints_nonempty, subset_affineSpan, subset_spanPoints, vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan, vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan, vectorSpan_add_self, vectorSpan_def, vectorSpan_empty, vectorSpan_eq_bot_iff_subsingleton, vectorSpan_insert_eq_vectorSpan, vectorSpan_mono, vectorSpan_of_subsingleton, vectorSpan_singleton, vsub_mem_vectorSpan, vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan, vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints, vsub_mem_vectorSpan_pair, vsub_rev_mem_vectorSpan_pair, vsub_set_subset_vectorSpan	134
Total	148

AffineSubspace

Definitions

Name	Category	Theorems
carrier 📖	CompOp	—
direction 📖	CompOp	226 math math: Affine.Simplex.altitudeFoot_restrict, direction_inf, coe_vsub, direction_sup_eq_sup_direction, Affine.Simplex.orthogonalProjectionSpan_map, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, AffineMap.restrict.bijective, Affine.Simplex.finiteDimensional_direction_altitude, direction_affineSpan, Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, direction_inf_of_mem, Affine.Simplex.restrict_reindex, Affine.Simplex.faceOppositeCentroid_restrict, EuclideanGeometry.orthogonalProjection_congr, direction_le, AffineIsometryEquiv.ofTop_apply, finiteDimensional_direction_affineSpan_of_finite, Affine.Simplex.restrict_map_restrict, EuclideanGeometry.orthogonalProjection_contLinear, EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq, coe_subtypeA, subtype_apply, direction_eq_top_iff_of_nonempty, EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection, EuclideanGeometry.inter_eq_singleton_orthogonalProjection, linear_topEquiv, Affine.Simplex.orthogonalProjectionSpan_eq_point, EuclideanGeometry.orthogonalProjection_map, vsub_mem_direction, Affine.Simplex.circumradius_restrict, Affine.Simplex.medial_restrict, EuclideanGeometry.angle_orthogonalProjection_self, EuclideanGeometry.orthogonalProjection_apply_mem, coe_subtypeₐᵢ, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq, direction_affineSpan_insert, Affine.Simplex.finrank_direction_altitude, Submodule.toAffineSubspace_direction, Affine.Simplex.ninePointCircle_restrict, Affine.Simplex.face_restrict, finrank_vectorSpan_insert_le, Affine.Simplex.interior_restrict, inclusion_linear, EuclideanGeometry.orthogonalProjection_apply', Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, EuclideanGeometry.Sphere.coe_secondInter, finiteDimensional_direction_map, EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le, EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, Affine.Triangle.dist_circumcenter_reflection_orthocenter, AffineIsometryEquiv.coe_ofEq_apply, Affine.Simplex.altitude_restrict_eq_comap_subtype, isometryEquivMap.toAffineMap_eq, signedInfDist_eq_signedDist_of_mem, Affine.Simplex.signedInfDist_apply_self, signedInfDist_eq_signedDist_orthogonalProjection, AffineEquiv.linear_ofEq, coe_direction_eq_vsub_set, AffineIsometryEquiv.ofTop_symm_apply_coe, Collinear.finiteDimensional_direction_affineSpan, finiteDimensional_direction_affineSpan_insert_set, Affine.Simplex.orthogonalProjectionSpan_congr, mem_direction_iff_eq_vsub, AffineIsometryEquiv.ofEq_symm, Affine.Simplex.vectorSpan_isOrtho_altitude_direction, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, asymptoticCone_affineSubspace, Coplanar.finiteDimensional_direction_affineSpan, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection, EuclideanGeometry.orthogonalProjection_subtype, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, finiteDimensional_direction_affineSpan_insert, Affine.Simplex.ExcenterExists.excenter_restrict, toContinuousAffineMap_subtypeₐᵢ, finiteDimensional_direction_affineSpan_range, Parallel.direction_eq, Affine.Triangle.dist_orthocenter_reflection_circumcenter, EuclideanGeometry.oangle_orthogonalProjection_self, Affine.Simplex.map_altitude_restrict, Affine.Simplex.faceOpposite_restrict, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, Affine.Simplex.exradius_restrict, EuclideanGeometry.reflection_apply_of_mem, direction_sup, Affine.Simplex.orthogonalProjection_circumcenter, direction_iInf_of_mem, subtypeA_toAffineMap, Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, Affine.Simplex.direction_mongePlane, coe_vadd, Affine.Simplex.circumcenter_restrict, AffineMap.restrict.injective, Affine.Simplex.height_restrict, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, subtype_injective, subtype_linear, pointwise_vadd_direction, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, topEquiv_symm_apply_coe, isometryEquivMap.coe_apply, EuclideanGeometry.Sphere.direction_orthRadius_le_iff, EuclideanGeometry.eq_or_eq_reflection_of_dist_eq, Affine.Simplex.incenter_restrict, EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, eq_iff_direction_eq_of_mem, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, EuclideanGeometry.dist_orthogonalProjection_eq_infNndist, direction_iInf, AffineMap.restrict.surjective, Affine.Simplex.inradius_restrict, subtypeₐᵢ_linear, map_direction, AffineMap.restrict.coe_apply, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, direction_top, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, Affine.Simplex.centroid_restrict, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, direction_lt_of_nonempty, EuclideanGeometry.orthogonalProjection_mem, Affine.Simplex.orthogonalProjectionSpan_restrict, direction_eq_vectorSpan, Affine.Simplex.setInterior_restrict, finiteDimensional_sup, Affine.Simplex.excenterWeights_restrict, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, AffineEquiv.ofEq_symm, AffineMap.restrict.linear_aux, EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq, linear_equivMapOfInjective, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, Affine.Simplex.median_restrict, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, affineSpan_coe_preimage_eq_top, direction_affineSpan_pair_le_iff_exists_smul, coe_direction_eq_vsub_set_left, EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq, Affine.Simplex.closedInterior_restrict, direction_sInf, EuclideanGeometry.orthogonalProjection_orthogonalProjection, EuclideanGeometry.orthogonalProjection_vsub_mem_direction, finiteDimensional_direction_affineSpan_image_of_finite, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, topEquiv_apply, Affine.Simplex.mongePoint_restrict, direction_iInf_of_mem_iInf, direction_sInf_of_mem, Affine.Simplex.eulerPoint_restrict, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, coe_inclusion_apply, Affine.Simplex.ExcenterExists.touchpoint_restrict, signedInfDist_singleton, Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, vadd_mem_iff_mem_direction, Affine.Simplex.excenterWeightsUnnorm_restrict, subtypeₐᵢ_linearIsometry, direction_bot, EuclideanGeometry.Sphere.IsTangent.isTangentAt, sup_direction_le, EuclideanGeometry.reflection_apply', AffineIsometryEquiv.ofEq_rfl, EuclideanGeometry.oangle_self_orthogonalProjection, AffineEquiv.coe_ofEq_apply, direction_inf_of_mem_inf, mem_direction_iff_eq_vsub_right, AffineMap.restrict.linear, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, direction_smul, coe_subtype, Affine.Simplex.orthogonalProjectionSpan_reindex, directionOfNonempty_eq_direction, EuclideanGeometry.orthogonalProjection_linear, signedInfDist_def, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, Affine.Simplex.signedInfDist_affineCombination, EuclideanGeometry.angle_self_orthogonalProjection, direction_perpBisector, angle_coe, EuclideanGeometry.orthogonalProjection_eq_self_iff, EuclideanGeometry.reflection_subtype, isometryEquivMap.apply_symm_apply, inclusion_rfl, direction_mk', EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal, vsub_right_mem_direction_iff_mem, EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace, EuclideanGeometry.orthogonalProjection_apply, EuclideanGeometry.Sphere.direction_orthRadius, signedInfDist_apply_self, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, EuclideanGeometry.orthogonalProjection_mem_orthogonal, mem_direction_iff_eq_vsub_left, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, equivMapOfInjective_toFun, direction_sInf_of_mem_sInf, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem, Affine.Simplex.map_subtype_restrict, Affine.Simplex.restrict_map_subtype, subtypeₐᵢ_toAffineMap, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, Affine.Simplex.affineSpan_pair_eq_altitude_iff, Affine.Simplex.direction_altitude, Affine.Simplex.restrict_map_inclusion, finiteDimensional_direction_affineSpan_singleton, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, EuclideanGeometry.orthogonalProjection_eq_iff_mem, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, sup_direction_lt_of_nonempty_of_inter_empty, vsub_left_mem_direction_iff_mem, mk'_eq, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, EuclideanGeometry.reflection_apply, AffineEquiv.ofEq_rfl, EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq, EuclideanGeometry.Sphere.finrank_orthRadius, isClosed_direction_iff, coe_direction_eq_vsub_set_right, Affine.Simplex.altitude_def, Affine.Simplex.restrict_points_coe, Affine.Simplex.excenterExists_restrict, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self
directionOfNonempty 📖	CompOp	1 math math: directionOfNonempty_eq_direction
gi 📖	CompOp	—
instCompleteLattice 📖	CompOp	90 math math: direction_inf, direction_sup_eq_sup_direction, direction_inf_of_mem, AffineBasis.tot, IsOpen.exists_subset_affineIndependent_span_eq_top, mem_sInf_iff, comap_bot, bot_lt_affineSpan, AffineEquiv.span_eq_top_iff, direction_eq_top_iff_of_nonempty, affineSpan_singleton_union_vadd_eq_top_of_span_eq_top, interior_convexHull_nonempty_iff_affineSpan_eq_top, linear_topEquiv, not_wSameSide_bot, span_iUnion, AffineBasis.tot', coe_eq_univ_iff, affineSpan_eq_sInf, EuclideanGeometry.Sphere.orthRadius_center, not_sSameSide_bot, AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv, mem_iInf_iff, bot_coe, Convex.interior_nonempty_iff_affineSpan_eq_top, parallel_bot_iff_eq_bot, map_inf_eq, span_union, smul_bot, Affine.Simplex.mongePlane_def, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, mem_top, smul_top, AffineIndependent.inf_affineSpan_eq_affineSpan_inter, direction_sup, direction_iInf_of_mem, mk'_top, affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, topEquiv_symm_apply_coe, nonempty_sup_left, AffineMap.map_top_of_surjective, direction_iInf, coe_eq_bot_iff, direction_top, Affine.Simplex.span_eq_top, isEmpty_bot, exists_subset_affineIndependent_affineSpan_eq_top, perpBisector_eq_top, map_inf_le, pointwise_vadd_bot, finiteDimensional_sup, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one, not_sOppSide_bot, IsOpen.exists_between_affineIndependent_span_eq_top, top_coe, affineSpan_coe_preimage_eq_top, pointwise_vadd_top, nonempty_sup_right, perpBisector_self, span_empty, map_bot, affineSpan_eq_top_of_nonempty_interior, direction_sInf, instIsSimpleOrderOfSubsingleton, topEquiv_apply, direction_sInf_of_mem, span_univ, map_eq_bot_iff, direction_bot, AffineBasis.isUnit_toMatrix_iff, sup_direction_le, instNonemptySubtypeMemTop, affineSpan_eq_bot, comap_supr, map_sup, comap_top, mem_inf_iff, coe_iInf, affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, IsOpen.affineSpan_eq_top, not_wOppSide_bot, EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq, eq_bot_or_nonempty, map_iSup, bot_parallel_iff_eq_bot, sup_direction_lt_of_nonempty_of_inter_empty, notMem_bot, Affine.Simplex.altitude_def, comap_inf, coe_sInf, affineSpan_eq_top_iff_nonempty_of_subsingleton
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	29 math math: AffineMap.restrict.bijective, affineSpan_le_toAffineSubspace_span, bot_lt_affineSpan, Affine.Simplex.affineSpan_face_le, le_def', affineSpan_pair_le_of_mem_of_mem, le_def, lt_def, affineSpan_le, Affine.Simplex.affineSpan_faceOpposite_le, Affine.Triangle.affineSpan_orthocenter_point_le_altitude, EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, AffineMap.restrict.surjective, affineSpan_pair_le_of_left_mem, affineSpan_le_of_subset_coe, map_comap_le, map_inf_le, gc_map_comap, instIsSimpleOrderOfSubsingleton, not_le_iff_exists, affineSpan_pair_le_of_right_mem, EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iff, map_le_iff_le_comap, le_comap_map, affineSpan_mono, inclusion_rfl, Affine.Simplex.map_subtype_restrict, Affine.Simplex.restrict_map_subtype, lt_iff_le_and_exists
instSetLike 📖	CompOp	330 math math: Affine.Simplex.altitudeFoot_restrict, Affine.Simplex.faceOppositeCentroid_mem_affineSpan_face, coe_vsub, Affine.Simplex.orthogonalProjectionSpan_map, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, AffineMap.restrict.bijective, Isometry.preimage_perpBisector, Submodule.mem_toAffineSubspace, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_face, self_mem_mk', mem_perpBisector_iff_inner_eq_zero', Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_faceOpposite, smul_mem_smul_iff₀, Affine.Simplex.circumcenter_mem_affineSpan, Affine.Simplex.restrict_reindex, Affine.Simplex.excenter_singleton_mem_affineSpan_range, Affine.Simplex.faceOppositeCentroid_restrict, EuclideanGeometry.orthogonalProjection_congr, AffineIsometryEquiv.ofTop_apply, mem_sInf_iff, AffineMap.eqOn_affineSpan, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_right, left_mem_perpBisector, EuclideanGeometry.preimage_inversion_perpBisector_inversion, SSameSide.right_notMem, AffineMap.lineMap_rev_mem_affineSpan_pair, vadd_right_mem_affineSpan_pair, Affine.Simplex.restrict_map_restrict, EuclideanGeometry.orthogonalProjection_contLinear, WSameSide.nonempty, coe_subtypeA, Affine.Simplex.point_mem_median, subtype_apply, EuclideanGeometry.Sphere.mem_tangentsFrom_iff, vadd_mem_mk', smul_vsub_rev_vadd_mem_affineSpan_pair, EuclideanGeometry.inter_eq_singleton_orthogonalProjection, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff', Sbtw.left_mem_affineSpan, linear_topEquiv, Affine.Simplex.orthogonalProjectionSpan_eq_point, EuclideanGeometry.orthogonalProjection_map, Collinear.mem_affineSpan_of_mem_of_ne, Affine.Simplex.circumradius_restrict, Affine.Simplex.ExcenterExists.touchpoint_notMem_affineSpan_of_ne, Affine.Simplex.medial_restrict, wOppSide_iff_exists_wbtw, SOppSide.nonempty, AffineIndependent.mem_affineSpan_iff, coe_subtypeₐᵢ, EuclideanGeometry.Sphere.IsTangentAt.mem_space, mem_perpBisector_iff_inner_eq_zero, perpBisector_nonempty, Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl, sSameSide_self_iff, Affine.Simplex.mongePoint_mem_mongePlane, wOppSide_self_iff, coe_eq_univ_iff, affineCombination_mem_affineSpan_pair, mem_intrinsicFrontier, Affine.Simplex.ninePointCircle_restrict, le_def', Affine.Simplex.face_restrict, affineSpan_eq_sInf, finrank_vectorSpan_insert_le, coe_smul, Affine.Simplex.interior_restrict, inclusion_linear, EuclideanGeometry.orthogonalProjection_apply', EuclideanGeometry.Sphere.coe_secondInter, EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le, mem_affineSpan_iff_eq_affineCombination, EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, affineCombination_mem_affineSpan, le_def, mem_iInf_iff, EuclideanGeometry.preimage_inversion_perpBisector, WOppSide.nonempty, bot_coe, Isometry.mapsTo_perpBisector, AffineIsometryEquiv.coe_ofEq_apply, inf_coe, Affine.Simplex.altitude_restrict_eq_comap_subtype, isometryEquivMap.toAffineMap_eq, lt_def, Affine.Simplex.signedInfDist_apply_self, Affine.Simplex.centroid_notMem_affineSpan_of_ne_univ, coe_inf, wSameSide_and_wOppSide_iff, signedInfDist_eq_signedDist_orthogonalProjection, AffineEquiv.linear_ofEq, coe_pointwise_vadd, Affine.Simplex.incenter_notMem_affineSpan_face, AffineIsometryEquiv.ofTop_symm_apply_coe, Affine.Simplex.orthogonalProjectionSpan_congr, EuclideanGeometry.image_inversion_perpBisector, AffineIsometryEquiv.ofEq_symm, SOppSide.right_notMem, EuclideanGeometry.reflection_eq_self_iff, Affine.Simplex.altitudeFoot_mem_affineSpan, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, affineSpan_le, smul_vsub_vadd_mem_affineSpan_pair, right_mem_affineSpan_pair, instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection, mem_top, mem_affineSpan_pair_iff_exists_lineMap_rev_eq, EuclideanGeometry.image_inversion_sphere_dist_center, EuclideanGeometry.orthogonalProjection_subtype, finiteDimensional_direction_affineSpan_insert, Affine.Simplex.ExcenterExists.excenter_restrict, Affine.Simplex.points_mem_affineSpan_face, closed_of_finiteDimensional, toContinuousAffineMap_subtypeₐᵢ, Affine.Simplex.points_mem_affineSpan_faceOpposite, mem_affineSpan, Affine.Simplex.circumsphere_unique_dist_eq, smul_mem_smul_iff_of_isUnit, EuclideanGeometry.preimage_inversion_sphere_dist_center, Affine.Simplex.map_altitude_restrict, Affine.Simplex.faceOpposite_restrict, convex, affineSpan_subset_span, Affine.Simplex.exradius_restrict, Affine.Simplex.orthogonalProjection_circumcenter, centroid_mem_affineSpan_of_nonempty, subtypeA_toAffineMap, vadd_mem_iff_mem_of_mem_direction, mem_map, mem_map_iff_mem_of_injective, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, Affine.Simplex.touchpoint_mem_affineSpan, coe_vadd, Affine.Simplex.altitudeFoot_mem_altitude, coe_affineSpan, Affine.Simplex.circumcenter_restrict, AffineMap.restrict.injective, Affine.Simplex.height_restrict, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, subtype_injective, subtype_linear, affineCombination_mem_affineSpan_image, EuclideanGeometry.Sphere.mem_of_mem_tangentsFrom, topEquiv_symm_apply_coe, isometryEquivMap.coe_apply, Affine.Simplex.mem_affineSpan_image_iff, mem_comap, nonempty_sup_left, centroid_mem_affineSpan_of_cast_card_ne_zero, intrinsicClosure_eq_closure_inter_affineSpan, exists_of_lt, EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq, wSameSide_self_iff, Affine.Simplex.incenter_restrict, mem_perpBisector_iff_inner_eq_inner, EuclideanGeometry.Sphere.IsTangent.infDist_eq_radius, mk'_nonempty, mem_affineSpan_pair_iff_exists_lineMap_eq, EuclideanGeometry.Sphere.IsTangent.notMem_of_dist_lt, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter, EuclideanGeometry.dist_orthogonalProjection_eq_infNndist, coe_eq_bot_iff, SOppSide.left_notMem, MeasureTheory.Measure.addHaar_affineSubspace, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_pair, AffineMap.restrict.surjective, Affine.Simplex.inradius_restrict, subtypeₐᵢ_linear, AffineMap.restrict.coe_apply, mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd, mem_affineSpan_iff_exists, subset_affineSpan, left_mem_affineSpan_pair, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, isEmpty_bot, Affine.Simplex.centroid_restrict, mem_perpBisector_iff_dist_eq', Affine.Simplex.ninePointCircle_center_mem_affineSpan, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, EuclideanGeometry.orthogonalProjection_mem, Affine.Simplex.orthogonalProjectionSpan_restrict, midpoint_mem_perpBisector, direction_eq_vectorSpan, EuclideanGeometry.Sphere.center_mem_orthRadius_iff, Affine.Simplex.setInterior_restrict, Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range, ext_iff, Affine.Triangle.orthocenter_mem_altitude, Affine.Simplex.excenterWeights_restrict, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, AffineEquiv.ofEq_symm, smul_mem_smul_iff, linear_equivMapOfInjective, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, top_coe, Affine.Simplex.median_restrict, Affine.Simplex.points_notMem_affineSpan_faceOpposite, EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan, affineSpan_coe_preimage_eq_top, nonempty_sup_right, EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq, Affine.Simplex.closedInterior_restrict, Affine.Simplex.incenter_mem_affineSpan_range, EuclideanGeometry.orthogonalProjection_orthogonalProjection, vectorSpan_add_self, not_le_iff_exists, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, Affine.Simplex.incenter_notMem_affineSpan_pair, preimage_coe_affineSpan_singleton, topEquiv_apply, affineSegment_subset_affineSpan, Affine.Simplex.mongePoint_restrict, mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero, affineCombination_mem_affineSpan_of_nonempty, Affine.Simplex.eulerPoint_restrict, Affine.Simplex.faceOppositeCentroid_mem_median, coe_inclusion_apply, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff, Affine.Simplex.ExcenterExists.touchpoint_restrict, affineSpan_nonempty, Affine.Simplex.excenterWeightsUnnorm_restrict, subtypeₐᵢ_linearIsometry, Affine.Triangle.orthocenter_mem_affineSpan, Affine.Simplex.mongePoint_mem_affineSpan, EuclideanGeometry.Sphere.IsTangent.isTangentAt, instNonemptySubtypeMemTop, IsClosed.convexHull_subset_affineSpan_isVisible, mem_perpBisector_iff_dist_eq, EuclideanGeometry.reflection_apply', AffineIsometryEquiv.ofEq_rfl, mem_fintypeAffineCoords_iff_sum, Affine.Simplex.centroid_mem_median, AffineEquiv.coe_ofEq_apply, EuclideanGeometry.Sphere.isTangentAt_center_iff, AffineMap.restrict.linear, instNonemptySubtypeMemMk', coe_subtype, Affine.Simplex.orthogonalProjectionSpan_reindex, Affine.Simplex.touchpoint_empty_notMem_affineSpan_of_ne, EuclideanGeometry.orthogonalProjection_linear, signedInfDist_def, vadd_mem_pointwise_vadd_iff, Affine.Simplex.mem_altitude, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, centroid_mem_affineSpan_of_card_eq_add_one, mem_mk', mem_affineSpan_singleton, Affine.Simplex.signedInfDist_affineCombination, EuclideanGeometry.Sphere.mem_commonIntTangents_iff, angle_coe, mem_inf_iff, EuclideanGeometry.orthogonalProjection_eq_self_iff, mem_perpBisector_iff_inner_eq, EuclideanGeometry.reflection_subtype, Set.Nonempty.affineSpan, isometryEquivMap.apply_symm_apply, SSameSide.left_notMem, inclusion_rfl, coe_injective, SOppSide.exists_sbtw, coe_iInf, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal, Affine.Simplex.setInterior_subset_affineSpan, Affine.Simplex.touchpoint_mem_affineSpan_simplex, EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace, Sbtw.right_mem_affineSpan, EuclideanGeometry.orthogonalProjection_apply, AffineIndependent.affineSpan_disjoint_of_disjoint, AffineIndependent.existsUnique_dist_eq, signedInfDist_apply_self, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, EuclideanGeometry.orthogonalProjection_mem_orthogonal, Wbtw.mem_affineSpan, mem_intrinsicInterior, nonempty_map, centroid_mem_affineSpan_of_card_ne_zero, equivMapOfInjective_toFun, instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem, Wbtw.left_mem_affineSpan_of_right_ne, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem, eq_bot_or_nonempty, Affine.Simplex.map_subtype_restrict, mem_finsuppAffineCoords_iff_linearCombination, Wbtw.right_mem_affineSpan_of_left_ne, Affine.Simplex.restrict_map_subtype, AffineIndependent.notMem_affineSpan_diff, subtypeₐᵢ_toAffineMap, mem_perpBisector_pointReflection_iff_inner_eq_zero, mem_coe, Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite, AffineMap.lineMap_mem_affineSpan_pair, Affine.Simplex.affineSpan_pair_eq_altitude_iff, Affine.Simplex.closedInterior_subset_affineSpan, Affine.Simplex.restrict_map_inclusion, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, EuclideanGeometry.orthogonalProjection_eq_iff_mem, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, affineSpan_insert_affineSpan, coe_comap, nonempty_iff_ne_bot, SSameSide.nonempty, affineSpan_insert_zero, Affine.Simplex.incenter_notMem_affineSpan_faceOpposite, convexHull_subset_affineSpan, affineSpan_coe, right_mem_perpBisector, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, EuclideanGeometry.reflection_apply, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left, Affine.Simplex.centroid_mem_affineSpan, AffineEquiv.ofEq_rfl, notMem_bot, isClosed_direction_iff, finiteDimensional_vectorSpan_insert, coe_affineSpan_singleton, EuclideanGeometry.Sphere.infDist_eq_radius_iff_isTangent, vadd_left_mem_affineSpan_pair, intrinsicClosure_subset_affineSpan, lt_iff_le_and_exists, Affine.Simplex.restrict_points_coe, EuclideanGeometry.Sphere.self_mem_orthRadius, Affine.Simplex.excenterExists_restrict, coe_sInf, mem_intrinsicClosure, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self, coe_map
mk' 📖	CompOp	13 math math: self_mem_mk', vadd_mem_mk', EuclideanGeometry.inter_eq_singleton_orthogonalProjection, map_mk', Affine.Simplex.mongePlane_def, mk'_top, mk'_nonempty, instNonemptySubtypeMemMk', mem_mk', direction_mk', EuclideanGeometry.orthogonalProjection_mem_orthogonal, mk'_eq, Affine.Simplex.altitude_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_coe 📖	mathematical	—	affineSpan SetLike.coe AffineSubspace instSetLike	—	le_antisymm vadd_mem_of_mem_direction subset_affineSpan
affineSpan_eq_sInf 📖	mathematical	—	affineSpan InfSet.sInf AffineSubspace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice setOf Set Set.instHasSubset SetLike.coe instSetLike	—	le_antisymm affineSpan_le_of_subset_coe Set.subset_iInter₂ sInf_le subset_spanPoints
affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty 📖	mathematical	Set.Nonempty	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder vectorSpan Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instTop	—	vectorSpan_eq_top_of_affineSpan_eq_top mem_affineSpan eq_iff_direction_eq_of_mem mem_top direction_affineSpan direction_top
affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial 📖	mathematical	—	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder vectorSpan Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instTop	—	Set.eq_empty_or_nonempty span_empty instNontrivial vectorSpan_empty AddTorsor.subsingleton_iff affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty
bot_coe 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set Set.instEmptyCollection	—	—
bot_ne_top 📖	—	—	—	—	Set.empty_ne_univ AddTorsor.nonempty top_coe bot_coe ext_iff
card_pos_of_affineSpan_eq_top 📖	mathematical	affineSpan Set.range Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Fintype.card	—	nonempty_of_affineSpan_eq_top Fintype.card_pos_iff
coe_direction_eq_vsub_set 📖	mathematical	Set.Nonempty SetLike.coe AffineSubspace instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction VSub.vsub Set Set.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	directionOfNonempty_eq_direction
coe_direction_eq_vsub_set_left 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction Set.image VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	Set.ext SetLike.mem_coe Submodule.neg_mem_iff coe_direction_eq_vsub_set_right Set.mem_image neg_vsub_eq_vsub_rev
coe_direction_eq_vsub_set_right 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction Set.image VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	coe_direction_eq_vsub_set le_antisymm vadd_mem_of_mem_direction vsub_mem_direction vadd_vsub
coe_eq_bot_iff 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike Set Set.instEmptyCollection Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	coe_injective bot_coe
coe_eq_univ_iff 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike Set.univ Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	coe_injective top_coe
coe_iInf 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.iInter	—	iInf.eq_1 coe_sInf Set.biInter_range
coe_inf 📖	mathematical	—	Set SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.coe AffineSubspace instSetLike Set.instInter	—	—
coe_injective 📖	mathematical	—	AffineSubspace Set SetLike.coe instSetLike	—	SetLike.coe_injective
coe_sInf 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.iInter Set Set.instMembership	—	—
directionOfNonempty_eq_direction 📖	mathematical	Set.Nonempty SetLike.coe AffineSubspace instSetLike	directionOfNonempty direction	—	le_antisymm SetLike.coe_subset_coe instIsConcreteLE directionOfNonempty.eq_1 direction.eq_1 vsub_set_subset_vectorSpan Submodule.span_le Set.Subset.rfl
direction_bot 📖	mathematical	—	direction Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	direction_eq_vectorSpan bot_coe vectorSpan_def Set.vsub_empty Submodule.span_empty
direction_eq_top_iff_of_nonempty 📖	mathematical	Set.Nonempty SetLike.coe AffineSubspace instSetLike	direction Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instTop OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext_of_direction_eq direction_top Set.inter_univ
direction_eq_vectorSpan 📖	mathematical	—	direction vectorSpan SetLike.coe AffineSubspace instSetLike	—	—
direction_iInf 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder direction iInf AffineSubspace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Submodule.instInfSet	—	LE.le.trans_eq direction_sInf iInf_range
direction_iInf_of_mem 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	direction iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet	—	iInf.eq_1 direction_sInf_of_mem Set.forall_mem_range iInf_range
direction_iInf_of_mem_iInf 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	direction Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet	—	iInf.eq_1 direction_sInf_of_mem_sInf iInf_range
direction_inf 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder direction AffineSubspace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Submodule.instMin	—	le_inf sInf_le_sInf trans Set.instIsTransSubset Set.vsub_self_mono Set.inter_subset_left Set.inter_subset_right
direction_inf_of_mem 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	direction SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instMin	—	Submodule.ext Submodule.mem_inf vadd_mem_iff_mem_direction mem_inf_iff
direction_inf_of_mem_inf 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	direction Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instMin	—	direction_inf_of_mem mem_inf_iff
direction_le 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder direction	—	vectorSpan_mono
direction_mk' 📖	mathematical	—	direction mk'	—	Submodule.ext mem_direction_iff_eq_vsub mk'_nonempty vsub_sub_vsub_cancel_right Submodule.sub_mem vadd_mem_mk' self_mem_mk' vadd_vsub
direction_sInf 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder direction InfSet.sInf AffineSubspace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice iInf Submodule.instInfSet Set Set.instMembership	—	iInf_congr_Prop le_iInf₂ Submodule.span_mono Set.vsub_self_mono Set.biInter_subset_of_mem
direction_sInf_of_mem 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	direction InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice iInf Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Set Set.instMembership	—	LE.le.antisymm direction_sInf vadd_mem_iff_mem_direction mem_sInf_iff
direction_sInf_of_mem_sInf 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	direction iInf Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Set Set.instMembership	—	direction_sInf_of_mem mem_sInf_iff
direction_top 📖	mathematical	—	direction Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instTop	—	AddTorsor.nonempty Submodule.ext Submodule.mem_top vsub_mem_direction mem_top vadd_vsub
eq_bot_or_nonempty 📖	mathematical	—	Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set.Nonempty SetLike.coe instSetLike	—	nonempty_iff_ne_bot eq_or_ne
eq_iff_direction_eq_of_mem 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	direction	—	ext_of_direction_eq
eq_of_direction_eq_of_nonempty_of_le 📖	—	direction Set.Nonempty SetLike.coe AffineSubspace instSetLike Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	—	ext_of_direction_eq
exists_of_lt 📖	mathematical	AffineSubspace Preorder.toLT PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike	—	Set.exists_of_ssubset
ext 📖	—	AffineSubspace SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike	—	SetLike.ext'_iff
ext_of_direction_eq 📖	—	direction Set.Nonempty Set Set.instInter SetLike.coe AffineSubspace instSetLike	—	—	ext Set.mem_of_mem_inter_left Set.Nonempty.some_mem Set.mem_of_mem_inter_right vsub_vadd vadd_mem_of_mem_direction vsub_mem_direction
inf_coe 📖	mathematical	—	Set SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.coe AffineSubspace instSetLike Set.instInter	—	coe_inf
instIsSimpleOrderOfSubsingleton 📖	mathematical	—	IsSimpleOrder AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder CompleteLattice.toBoundedOrder instCompleteLattice	—	instNontrivial coe_eq_bot_iff coe_eq_univ_iff Set.eq_empty_or_nonempty Set.Nonempty.eq_univ
instNonemptySubtypeMemMk' 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike mk'	—	self_mem_mk'
instNonemptySubtypeMemTop 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.instNonemptyTop AddTorsor.nonempty
instNontrivial 📖	mathematical	—	Nontrivial AffineSubspace	—	bot_ne_top
inter_eq_singleton_of_nonempty_of_isCompl 📖	mathematical	Set.Nonempty SetLike.coe AffineSubspace instSetLike IsCompl Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice direction	Set Set.instInter Set.instSingletonSet	—	inter_nonempty_of_nonempty_of_sup_direction_eq_top IsCompl.sup_eq_top Set.ext Set.mem_singleton_iff vsub_mem_direction vsub_eq_zero_iff_eq Submodule.mem_bot IsCompl.inf_eq_bot
inter_nonempty_of_nonempty_of_sup_direction_eq_top 📖	mathematical	Set.Nonempty SetLike.coe AffineSubspace instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice direction Top.top Submodule.instTop	Set Set.instInter	—	sup_direction_lt_of_nonempty_of_inter_empty Set.not_nonempty_iff_eq_empty not_top_lt
isEmpty_bot 📖	mathematical	—	IsEmpty AffineSubspace SetLike.instMembership instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Subtype.isEmpty_of_false notMem_bot
le_def 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder Set Set.instHasSubset SetLike.coe instSetLike	—	—
le_def' 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	—	—
lt_def 📖	mathematical	—	AffineSubspace Preorder.toLT PartialOrder.toPreorder instPartialOrder Set Set.instHasSSubset SetLike.coe instSetLike	—	—
lt_iff_le_and_exists 📖	mathematical	—	AffineSubspace Preorder.toLT PartialOrder.toPreorder instPartialOrder Preorder.toLE SetLike.instMembership instSetLike	—	lt_iff_le_not_ge not_le_iff_exists
mem_coe 📖	mathematical	—	Set Set.instMembership SetLike.coe AffineSubspace instSetLike SetLike.instMembership	—	—
mem_direction_iff_eq_vsub 📖	mathematical	Set.Nonempty SetLike.coe AffineSubspace instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	SetLike.mem_coe coe_direction_eq_vsub_set Set.mem_vsub
mem_direction_iff_eq_vsub_left 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	SetLike.mem_coe coe_direction_eq_vsub_set_left
mem_direction_iff_eq_vsub_right 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	SetLike.mem_coe coe_direction_eq_vsub_set_right
mem_iInf_iff 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	iInf.eq_1 mem_sInf_iff Set.forall_mem_range
mem_inf_iff 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	—
mem_mk' 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike mk' Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	—
mem_sInf_iff 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	Set.mem_iInter₂
mem_top 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.mem_univ
mk'_eq 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	mk' direction	—	ext_of_direction_eq direction_mk' Set.mem_inter self_mem_mk'
mk'_nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe AffineSubspace instSetLike mk'	—	self_mem_mk'
mk'_top 📖	mathematical	—	mk' Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instTop AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext
nonempty_iff_ne_bot 📖	mathematical	—	Set.Nonempty SetLike.coe AffineSubspace instSetLike	—	Set.nonempty_iff_ne_empty coe_eq_bot_iff
nonempty_of_affineSpan_eq_top 📖	mathematical	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Set.Nonempty	—	Set.nonempty_iff_ne_empty bot_ne_top span_empty
nonempty_sup_left 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	Nonempty.map SetLike.le_def instIsConcreteLE le_sup_left
nonempty_sup_right 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	Nonempty.map SetLike.le_def instIsConcreteLE le_sup_right
notMem_bot 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Set.notMem_empty
not_le_iff_exists 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	—	Set.not_subset
self_mem_mk' 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike mk'	—	vsub_self AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
smul_vsub_vadd_mem 📖	mathematical	Set Set.instMembership carrier	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	—
spanPoints_subset_coe_of_subset_coe 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace instSetLike	spanPoints	—	Set.mem_of_mem_of_subset vadd_mem_of_mem_direction vectorSpan_mono SetLike.mem_coe SetLike.le_def instIsConcreteLE
span_empty 📖	mathematical	—	affineSpan Set Set.instEmptyCollection Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	GaloisConnection.l_bot GaloisInsertion.gc
span_iUnion 📖	mathematical	—	affineSpan Set.iUnion iSup AffineSubspace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_iSup GaloisInsertion.gc
span_union 📖	mathematical	—	affineSpan Set Set.instUnion AffineSubspace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_sup GaloisInsertion.gc
span_univ 📖	mathematical	—	affineSpan Set.univ Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff subset_affineSpan
sup_direction_le 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice direction AffineSubspace instCompleteLattice	—	sup_le sInf_le_sInf Set.Subset.trans Set.vsub_self_mono le_sup_left le_sup_right
sup_direction_lt_of_nonempty_of_inter_empty 📖	mathematical	Set.Nonempty SetLike.coe AffineSubspace instSetLike Set Set.instInter Set.instEmptyCollection	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice direction instCompleteLattice	—	SetLike.lt_iff_le_and_exists instIsConcreteLE sup_direction_le vsub_mem_direction le_sup_right le_sup_left Submodule.mem_sup Set.Nonempty.ne_empty vadd_mem_of_mem_direction vsub_eq_zero_iff_eq vsub_vadd_eq_vsub_sub sub_eq_add_neg add_comm neg_neg vadd_vsub_assoc add_assoc neg_vsub_eq_vsub_rev sub_eq_zero Submodule.neg_mem
top_coe 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.univ	—	—
vadd_mem_iff_mem_direction 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction	—	vadd_vsub vsub_mem_direction vadd_mem_of_mem_direction
vadd_mem_iff_mem_of_mem_direction 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction	AffineSubspace instSetLike HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	neg_vadd_vadd vadd_mem_of_mem_direction Submodule.neg_mem
vadd_mem_mk' 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike	AffineSubspace instSetLike mk' HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	vadd_vsub
vadd_mem_of_mem_direction 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction AffineSubspace instSetLike	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	mem_direction_iff_eq_vsub one_smul smul_vsub_vadd_mem
vectorSpan_eq_top_of_affineSpan_eq_top 📖	mathematical	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	vectorSpan Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instTop	—	direction_affineSpan direction_top
vsub_mem_direction 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vsub_mem_vectorSpan

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan 📖	mathematical	Set.Nonempty	SetLike.coe AffineSubspace AffineSubspace.instSetLike affineSpan	—	affineSpan_nonempty

Submodule

Definitions

Name	Category	Theorems
toAffineSubspace 📖	CompOp	3 math math: mem_toAffineSubspace, affineSpan_le_toAffineSubspace_span, toAffineSubspace_direction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_toAffineSubspace 📖	mathematical	—	AffineSubspace addGroupIsAddTorsor AddCommGroup.toAddGroup SetLike.instMembership AffineSubspace.instSetLike toAffineSubspace Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid setLike	—	—
toAffineSubspace_direction 📖	mathematical	—	AffineSubspace.direction addGroupIsAddTorsor AddCommGroup.toAddGroup toAffineSubspace	—	ext AffineSubspace.vadd_mem_iff_mem_direction zero_mem add_zero

(root)

Definitions

Name	Category	Theorems
affineSpan 📖	CompOp	224 math math: Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, Affine.Simplex.isTangentAt_insphere_iff_eq_touchpoint, AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, Affine.Simplex.faceOppositeCentroid_mem_affineSpan_face, exists_affineIndependent, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff, Affine.Simplex.orthogonalProjectionSpan_map, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_face, affineSpan_le_toAffineSubspace_span, Affine.Simplex.sSameSide_excenter_singleton_point, AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul', direction_affineSpan, Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_faceOpposite, AffineBasis.tot, Affine.Simplex.circumcenter_mem_affineSpan, Affine.Simplex.affineSpan_pair_altitudeFoot_eq_altitude, Affine.Simplex.excenter_singleton_mem_affineSpan_range, IsOpen.exists_subset_affineIndependent_span_eq_top, AffineMap.eqOn_affineSpan, Affine.Triangle.sSameSide_affineSpan_pair_point_incenter, finiteDimensional_direction_affineSpan_of_finite, AffineMap.lineMap_rev_mem_affineSpan_pair, vadd_right_mem_affineSpan_pair, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff, Affine.Simplex.median_eq_line_point_centroid, bot_lt_affineSpan, AffineEquiv.span_eq_top_iff, smul_vsub_rev_vadd_mem_affineSpan_pair, affineSpan_singleton_union_vadd_eq_top_of_span_eq_top, interior_convexHull_nonempty_iff_affineSpan_eq_top, Sbtw.left_mem_affineSpan, Affine.Simplex.orthogonalProjectionSpan_eq_point, Affine.Simplex.sSameSide_incenter_point, Affine.Simplex.affineSpan_face_le, Collinear.mem_affineSpan_of_mem_of_ne, Affine.Simplex.ExcenterExists.touchpoint_notMem_affineSpan_of_ne, EuclideanGeometry.Sphere.isTangentAt_of_dist_sq_eq_power, AffineIndependent.mem_affineSpan_iff, AffineSubspace.span_iUnion, EuclideanGeometry.affineSpan_of_orthocentricSystem, affineSpan_eq_affineSpan_lineMap_units, AffineBasis.tot', Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl, AffineSubspace.direction_affineSpan_insert, Affine.Simplex.isTangentAt_insphere_touchpoint, affineCombination_mem_affineSpan_pair, Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, mem_intrinsicFrontier, AffineSubspace.affineSpan_eq_sInf, affineSpan_pair_le_of_mem_of_mem, Affine.Simplex.affineSpan_faceOpposite_eq_orthRadius_insphere, affineSpan_convexHull, mem_affineSpan_iff_eq_affineCombination, AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv, Affine.Triangle.dist_circumcenter_reflection_orthocenter, affineCombination_mem_affineSpan, Affine.Simplex.ExcenterExists.isTangentAt_touchpoint, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff, Convex.interior_nonempty_iff_affineSpan_eq_top, AffineSubspace.span_union, Affine.Simplex.signedInfDist_apply_self, Affine.Simplex.centroid_notMem_affineSpan_of_ne_univ, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, Affine.Simplex.ExcenterExists.sOppSide_excenter_point_iff, Affine.Simplex.incenter_notMem_affineSpan_face, Affine.Triangle.affineSpan_pair_eq_orthRadius, Collinear.finiteDimensional_direction_affineSpan, finiteDimensional_direction_affineSpan_insert_set, Affine.Simplex.orthogonalProjectionSpan_congr, Affine.Simplex.mongePlane_def, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff, Coplanar.finiteDimensional_direction_affineSpan, Affine.Simplex.altitudeFoot_mem_affineSpan, affineSpan_le, smul_vsub_vadd_mem_affineSpan_pair, right_mem_affineSpan_pair, mem_affineSpan_pair_iff_exists_lineMap_rev_eq, finiteDimensional_direction_affineSpan_insert, Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point, Affine.Simplex.points_mem_affineSpan_face, Affine.Simplex.points_mem_affineSpan_faceOpposite, finiteDimensional_direction_affineSpan_range, mem_affineSpan, Affine.Simplex.circumsphere_unique_dist_eq, Affine.Triangle.dist_orthocenter_reflection_circumcenter, affineSpan_subset_span, AffineIndependent.inf_affineSpan_eq_affineSpan_inter, Affine.Simplex.orthogonalProjection_circumcenter, Affine.Simplex.affineSpan_faceOpposite_le, centroid_mem_affineSpan_of_nonempty, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite, Affine.Simplex.touchpoint_mem_affineSpan, EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior, coe_affineSpan, Affine.Triangle.affineSpan_orthocenter_point_le_altitude, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two, affineCombination_mem_affineSpan_image, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, AffineSubspace.map_span, Affine.Simplex.sOppSide_excenter_singleton_point, Affine.Simplex.ExcenterExists.sOppSide_point_excenter_iff, Affine.Simplex.mem_affineSpan_image_iff, centroid_mem_affineSpan_of_cast_card_ne_zero, intrinsicClosure_eq_closure_inter_affineSpan, mem_affineSpan_pair_iff_exists_lineMap_eq, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter, Affine.Simplex.ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_pair, AffineSubspace.mem_affineSpan_insert_iff, Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere, mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd, mem_affineSpan_iff_exists, subset_affineSpan, left_mem_affineSpan_pair, Affine.Simplex.span_eq_top, exists_subset_affineIndependent_affineSpan_eq_top, affineSpan_le_of_subset_coe, Affine.Simplex.sOppSide_point_excenter_singleton, Affine.Simplex.ninePointCircle_center_mem_affineSpan, AffineSubspace.comap_span, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one, IsOpen.exists_between_affineIndependent_span_eq_top, Affine.Simplex.affineSpan_range_medial, Affine.Simplex.points_notMem_affineSpan_faceOpposite, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan, affineSpan_coe_preimage_eq_top, AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul, AffineSubspace.span_empty, affineSpan_eq_top_of_nonempty_interior, Affine.Simplex.incenter_mem_affineSpan_range, affineSpan_intrinsicClosure, vectorSpan_add_self, finiteDimensional_direction_affineSpan_image_of_finite, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, Affine.Simplex.incenter_notMem_affineSpan_pair, AffineSubspace.preimage_coe_affineSpan_singleton, affineSegment_subset_affineSpan, affineCombination_mem_affineSpan_of_nonempty, AffineSubspace.span_univ, Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton, AffineSubspace.signedInfDist_singleton, affineSpan_nonempty, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff, Affine.Triangle.orthocenter_mem_affineSpan, Affine.Simplex.mongePoint_mem_affineSpan, AffineBasis.isUnit_toMatrix_iff, IsClosed.convexHull_subset_affineSpan_isVisible, AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul, affineSpan_eq_bot, Affine.Simplex.orthogonalProjectionSpan_reindex, Affine.Simplex.touchpoint_empty_notMem_affineSpan_of_ne, EuclideanGeometry.Sphere.IsTangentAt_iff_angle_eq_pi_div_two, Affine.Simplex.sSameSide_point_excenter_singleton, Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, affineSpan_mono, centroid_mem_affineSpan_of_card_eq_add_one, EuclideanGeometry.Sphere.isTangentAt_iff_dist_sq_eq_power, AffineSubspace.mem_affineSpan_singleton, Affine.Simplex.signedInfDist_affineCombination, AffineIndependent.injective_affineSpan_image, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff, Set.Nonempty.affineSpan, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, Affine.Simplex.setInterior_subset_affineSpan, Affine.Simplex.touchpoint_mem_affineSpan_simplex, Sbtw.right_mem_affineSpan, AffineIndependent.affineSpan_disjoint_of_disjoint, EuclideanGeometry.existsUnique_dist_eq_of_insert, AffineIndependent.existsUnique_dist_eq, AffineSubspace.pointwise_vadd_span, IsOpen.affineSpan_eq_top, Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point, Wbtw.mem_affineSpan, mem_intrinsicInterior, centroid_mem_affineSpan_of_card_ne_zero, instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, Wbtw.left_mem_affineSpan_of_right_ne, Affine.Simplex.map_subtype_restrict, Wbtw.right_mem_affineSpan_of_left_ne, Affine.Simplex.restrict_map_subtype, AffineIndependent.notMem_affineSpan_diff, Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite, AffineMap.lineMap_mem_affineSpan_pair, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, Affine.Simplex.affineSpan_pair_eq_altitude_iff, Affine.Simplex.closedInterior_subset_affineSpan, finiteDimensional_direction_affineSpan_singleton, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, Collinear.affineSpan_eq_of_ne, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, affineSpan_insert_affineSpan, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, Affine.Triangle.sSameSide_affineSpan_pair_incenter_point, affineSpan_insert_zero, AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq, Affine.Simplex.incenter_notMem_affineSpan_faceOpposite, convexHull_subset_affineSpan, AffineSubspace.affineSpan_coe, Affine.Simplex.centroid_mem_affineSpan, AffineSubspace.affineSpan_pair_comm, Affine.Simplex.ExcenterExists.sSameSide_excenter_point_iff, AffineSubspace.coe_affineSpan_singleton, Affine.Simplex.altitude_def, vadd_left_mem_affineSpan_pair, intrinsicClosure_subset_affineSpan, mem_intrinsicClosure, affineSpan_eq_top_iff_nonempty_of_subsingleton, Affine.Simplex.sSameSide_point_incenter, Affine.Simplex.ExcenterExists.sSameSide_point_excenter_iff, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff, AffineSubspace.smul_span
spanPoints 📖	CompOp	5 math math: AffineSubspace.spanPoints_subset_coe_of_subset_coe, mem_spanPoints, spanPoints_nonempty, coe_affineSpan, subset_spanPoints
vectorSpan 📖	CompOp	81 math math: AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, vectorSpan_range_eq_span_range_vsub_left_ne, vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints, direction_affineSpan, vsub_mem_vectorSpan, finiteDimensional_vectorSpan_range, finrank_vectorSpan_image_finset_le, vsub_mem_vectorSpan_pair, vectorSpan_eq_bot_iff_subsingleton, vectorSpan_eq_span_vsub_set_right_ne, finrank_vectorSpan_le_iff_not_affineIndependent, mem_vectorSpan_iff_eq_weightedVSub, AffineIndependent.finrank_vectorSpan_add_one, vectorSpan_range_eq_span_range_vsub_right, AffineIndependent.card_le_finrank_succ, Coplanar.finrank_le_two, AffineSubspace.vectorSpan_union_of_mem_of_mem, finiteDimensional_vectorSpan_image_of_finite, finrank_vectorSpan_insert_le, vsub_rev_mem_vectorSpan_pair, vectorSpan_empty, collinear_iff_finrank_le_one, vectorSpan_image_eq_span_vsub_set_left_ne, finiteDimensional_vectorSpan_of_finite, AffineIndependent.vectorSpan_image_eq_iff, vectorSpan_eq_span_vsub_finset_right_ne, Affine.Simplex.vectorSpan_isOrtho_altitude_direction, affineIndependent_iff_not_finrank_vectorSpan_le, vectorSpan_pair_rev, AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one, vectorSpan_eq_span_vsub_set_left_ne, finiteDimensional_vectorSpan_insert_set, finiteDimensional_vectorSpan_singleton, vectorSpan_insert_eq_vectorSpan, AffineMap.map_vectorSpan, AffineIndependent.finrank_vectorSpan_image_finset, vectorSpan_pair, vectorSpan_mono, Affine.Simplex.direction_mongePlane, affineIndependent_iff_le_finrank_vectorSpan, vectorSpan_eq_span_vsub_set_left, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, vectorSpan_segment, Collinear.finiteDimensional_vectorSpan, mem_vectorSpan_pair_rev, mem_affineSpan_iff_exists, Real.Convex.dimH_eq_finrank_vectorSpan, collinear_iff_rank_le_one, Coplanar.finiteDimensional_vectorSpan, vectorSpan_range_eq_span_range_vsub_right_ne, vectorSpan_vadd, AffineSubspace.direction_eq_vectorSpan, weightedVSub_mem_vectorSpan, AffineIndependent.finrank_vectorSpan, vectorSpan_singleton, vectorSpan_def, smul_vsub_rev_mem_vectorSpan_pair, vectorSpan_add_self, mem_vectorSpan_pair, vectorSpan_image_eq_span_vsub_set_right_ne, Collinear.finrank_le_one, affineIndependent_iff_finrank_vectorSpan_eq, vectorSpan_eq_span_vsub_set_right, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, AffineSubspace.Parallel.vectorSpan_eq, smul_vsub_mem_vectorSpan_pair, finrank_vectorSpan_range_add_one_le, vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan, coplanar_iff_finrank_le_two, vsub_set_subset_vectorSpan, weightedVSub_mem_vectorSpan_pair, vectorSpan_range_eq_span_range_vsub_left, Affine.Simplex.direction_altitude, AffineMap.linear_eqOn_vectorSpan, AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq, AffineMap.vectorSpan_image_eq_submodule_map, AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top, finrank_vectorSpan_insert_le_set, finiteDimensional_vectorSpan_insert, finrank_vectorSpan_range_le, vectorSpan_of_subsingleton
«termLine[_,_,_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_eq_bot 📖	mathematical	—	affineSpan Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set Set.instEmptyCollection	—	not_iff_not AffineSubspace.nonempty_iff_ne_bot affineSpan_nonempty Set.nonempty_iff_ne_empty
affineSpan_eq_top_iff_nonempty_of_subsingleton 📖	mathematical	—	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.Nonempty	—	bot_lt_affineSpan IsSimpleOrder.bot_lt_iff_eq_top AffineSubspace.instIsSimpleOrderOfSubsingleton
affineSpan_induction 📖	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	—	affineSpan_le
affineSpan_induction' 📖	—	subset_affineSpan HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AffineSubspace.smul_vsub_vadd_mem affineSpan AffineSubspace SetLike.instMembership AffineSubspace.instSetLike	—	—	subset_affineSpan AffineSubspace.smul_vsub_vadd_mem affineSpan_induction
affineSpan_insert_affineSpan 📖	mathematical	—	affineSpan Set Set.instInsert SetLike.coe AffineSubspace AffineSubspace.instSetLike	—	Set.insert_eq AffineSubspace.span_union AffineSubspace.affineSpan_coe
affineSpan_insert_eq_affineSpan 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan	Set Set.instInsert	—	affineSpan_insert_affineSpan Set.insert_eq_of_mem AffineSubspace.mem_coe AffineSubspace.affineSpan_coe
affineSpan_insert_zero 📖	mathematical	—	SetLike.coe AffineSubspace addGroupIsAddTorsor AddCommGroup.toAddGroup AffineSubspace.instSetLike affineSpan Set Set.instInsert NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Submodule.span	—	Submodule.span_insert_zero HasSubset.Subset.antisymm Set.instAntisymmSubset affineSpan_subset_span vectorSpan_add_self vectorSpan_def Set.Subset.trans instIsConcreteLE Submodule.span_mono Set.subset_sub_left Set.mem_insert Set.subset_add_left
affineSpan_le 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set Set.instHasSubset SetLike.coe AffineSubspace.instSetLike	—	GaloisInsertion.gc
affineSpan_le_of_subset_coe 📖	mathematical	Set Set.instHasSubset SetLike.coe AffineSubspace AffineSubspace.instSetLike	Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan	—	AffineSubspace.spanPoints_subset_coe_of_subset_coe
affineSpan_le_toAffineSubspace_span 📖	mathematical	—	AffineSubspace addGroupIsAddTorsor AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Submodule.toAffineSubspace Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid	—	affineSpan_induction' Submodule.subset_span Submodule.add_mem Submodule.smul_mem Submodule.sub_mem
affineSpan_mono 📖	mathematical	Set Set.instHasSubset	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan	—	affineSpan_le_of_subset_coe Set.Subset.trans subset_affineSpan
affineSpan_nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe AffineSubspace AffineSubspace.instSetLike affineSpan	—	spanPoints_nonempty
affineSpan_pair_le_of_left_mem 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet	Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder	—	affineSpan_pair_le_of_mem_of_mem right_mem_affineSpan_pair
affineSpan_pair_le_of_mem_of_mem 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike	Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set Set.instInsert Set.instSingletonSet	—	affineSpan_le Set.insert_subset_iff Set.singleton_subset_iff
affineSpan_pair_le_of_right_mem 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet	Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder	—	affineSpan_pair_le_of_mem_of_mem left_mem_affineSpan_pair
affineSpan_subset_span 📖	mathematical	—	Set Set.instHasSubset SetLike.coe AffineSubspace addGroupIsAddTorsor AddCommGroup.toAddGroup AffineSubspace.instSetLike affineSpan Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Submodule.span	—	affineSpan_le_toAffineSubspace_span
bot_lt_affineSpan 📖	mathematical	—	AffineSubspace Preorder.toLT PartialOrder.toPreorder AffineSubspace.instPartialOrder Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder affineSpan Set.Nonempty	—	bot_lt_iff_ne_bot Set.nonempty_iff_ne_empty Iff.not affineSpan_eq_bot
coe_affineSpan 📖	mathematical	—	SetLike.coe AffineSubspace AffineSubspace.instSetLike affineSpan spanPoints	—	—
direction_affineSpan 📖	mathematical	—	AffineSubspace.direction affineSpan vectorSpan	—	le_antisymm Submodule.span_le vsub_vadd_eq_vsub_sub vadd_vsub_assoc Submodule.sub_mem Submodule.add_mem vsub_mem_vectorSpan vectorSpan_mono subset_spanPoints
instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan	—	Set.Nonempty.to_subtype Set.Nonempty.affineSpan Set.nonempty_coe_sort
left_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet	—	mem_affineSpan Set.mem_insert
mem_affineSpan 📖	mathematical	Set Set.instMembership	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan	—	mem_spanPoints
mem_affineSpan_iff_exists 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instMembership Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike vectorSpan HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	—
mem_spanPoints 📖	mathematical	Set Set.instMembership	spanPoints	—	Submodule.zero_mem zero_vadd
right_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet	—	mem_affineSpan Set.mem_insert_of_mem Set.mem_singleton
smul_vsub_mem_vectorSpan_pair 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan Set Set.instInsert Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction VSub.vsub AddTorsor.toVSub	—	Submodule.smul_mem vsub_mem_vectorSpan_pair
smul_vsub_rev_mem_vectorSpan_pair 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan Set Set.instInsert Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction VSub.vsub AddTorsor.toVSub	—	Submodule.smul_mem vsub_rev_mem_vectorSpan_pair
spanPoints_nonempty 📖	mathematical	—	Set.Nonempty spanPoints	—	Mathlib.Tactic.Contrapose.contrapose₁ Set.not_nonempty_iff_eq_empty vectorSpan_empty zero_vadd AddTorsor.nonempty Set.Nonempty.mono subset_spanPoints
subset_affineSpan 📖	mathematical	—	Set Set.instHasSubset SetLike.coe AffineSubspace AffineSubspace.instSetLike affineSpan	—	subset_spanPoints
subset_spanPoints 📖	mathematical	—	Set Set.instHasSubset spanPoints	—	mem_spanPoints
vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike vectorSpan	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan
vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan 📖	mathematical	Set Set.instMembership spanPoints Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	vadd_vadd Submodule.add_mem
vectorSpan_add_self 📖	mathematical	—	Set Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SetLike.coe Submodule Ring.toSemiring Submodule.setLike vectorSpan addGroupIsAddTorsor AddCommGroup.toAddGroup AffineSubspace AffineSubspace.instSetLike affineSpan	—	Set.ext
vectorSpan_def 📖	mathematical	—	vectorSpan Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub Set Set.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	—
vectorSpan_empty 📖	mathematical	—	vectorSpan Set Set.instEmptyCollection Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	vectorSpan_def Set.vsub_empty Submodule.span_empty
vectorSpan_eq_bot_iff_subsingleton 📖	mathematical	—	vectorSpan Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instBot Set.Subsingleton	—	Set.not_subsingleton_iff vsub_mem_vectorSpan vectorSpan_of_subsingleton
vectorSpan_insert_eq_vectorSpan 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan	vectorSpan Set Set.instInsert	—	affineSpan_insert_eq_affineSpan
vectorSpan_mono 📖	mathematical	Set Set.instHasSubset	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder vectorSpan	—	Submodule.span_mono Set.vsub_self_mono
vectorSpan_of_subsingleton 📖	mathematical	Set.Subsingleton	vectorSpan Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	Set.Subsingleton.eq_empty_or_singleton vectorSpan_empty vectorSpan_singleton
vectorSpan_singleton 📖	mathematical	—	vectorSpan Set Set.instSingletonSet Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	Set.singleton_vsub_singleton vsub_self Submodule.span_zero_singleton
vsub_mem_vectorSpan 📖	mathematical	Set Set.instMembership	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vsub_set_subset_vectorSpan Set.vsub_mem_vsub
vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike vectorSpan VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints
vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints 📖	mathematical	Set Set.instMembership spanPoints	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vsub_vadd_eq_vsub_sub vadd_vsub_assoc add_comm add_sub_assoc Submodule.sub_mem Submodule.add_mem vsub_mem_vectorSpan
vsub_mem_vectorSpan_pair 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan Set Set.instInsert Set.instSingletonSet VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vsub_mem_vectorSpan Set.mem_insert Set.mem_insert_of_mem Set.mem_singleton
vsub_rev_mem_vectorSpan_pair 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike vectorSpan Set Set.instInsert Set.instSingletonSet VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vsub_mem_vectorSpan Set.mem_insert_of_mem Set.mem_singleton Set.mem_insert
vsub_set_subset_vectorSpan 📖	mathematical	—	Set Set.instHasSubset VSub.vsub Set.vsub AddTorsor.toVSub AddCommGroup.toAddGroup SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike vectorSpan	—	Submodule.subset_span

---

← Back to Index