Basic

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean

Statistics

Metric	Count
Definitions closedInterior, face, faceOpposite, instInhabitedOfNatNat, interior, map, mkOfPoint, points, reindex, restrict, setInterior	11
Theorems affineCombination_mem_affineSpan_faceOpposite_iff, affineCombination_mem_closedInterior_face_iff_mem_Icc, affineCombination_mem_closedInterior_face_iff_nonneg, affineCombination_mem_closedInterior_iff, affineCombination_mem_interior_face_iff_mem_Ioo, affineCombination_mem_interior_face_iff_pos, affineCombination_mem_interior_iff, affineCombination_mem_setInterior_face_iff_mem, affineCombination_mem_setInterior_iff, affineSpan_faceOpposite_le, affineSpan_face_le, closedInterior_eq_singleton, closedInterior_map, closedInterior_reindex, closedInterior_restrict, closedInterior_subset_affineSpan, ext, ext_iff, faceOpposite_map, faceOpposite_point_eq_point_one, faceOpposite_point_eq_point_rev, faceOpposite_point_eq_point_succAbove, faceOpposite_point_eq_point_zero, faceOpposite_restrict, face_eq_mkOfPoint, face_map, face_points, face_points', face_restrict, independent, instNonemptyElemComplSetSingletonOfNontrivial, interior_eq_empty, interior_map, interior_reindex, interior_restrict, interior_ssubset_closedInterior, interior_subset_closedInterior, map_comp, map_id, map_mkOfPoint, map_points, map_subtype_restrict, mem_affineSpan_image_iff, mkOfPoint_points, nonempty, point_mem_closedInterior, point_notMem_interior, points_mem_affineSpan_face, points_mem_affineSpan_faceOpposite, points_notMem_affineSpan_faceOpposite, range_faceOpposite_points, range_faceOpposite_reindex, range_face_points, range_face_reindex, range_mkOfPoint_points, reindex_map, reindex_points, reindex_range_points, reindex_refl, reindex_reindex_symm, reindex_symm_reindex, reindex_trans, restrict_map_inclusion, restrict_map_restrict, restrict_map_subtype, restrict_points_coe, restrict_reindex, setInterior_map, setInterior_mono, setInterior_reindex, setInterior_restrict, setInterior_subset_affineSpan	72
Total	83

Affine.Simplex

Definitions

Name	Category	Theorems
closedInterior 📖	CompOp	18 math math: affineCombination_mem_closedInterior_iff, interior_subset_closedInterior, affineCombination_mem_closedInterior_face_iff_nonneg, isCompact_closedInterior, closedInterior_eq_affineSegment, mem_closedInterior_face_iff_wbtw, interior_ssubset_closedInterior, mem_closedInterior_iff_wbtw, closedInterior_restrict, closedInterior_face_eq_affineSegment, closedInterior_map, affineCombination_mem_closedInterior_face_iff_mem_Icc, point_mem_closedInterior, closedInterior_subset_affineSpan, convexHull_eq_closedInterior, closedInterior_reindex, closedInterior_eq_singleton, isClosed_closedInterior
face 📖	CompOp	22 math math: face_map, ExcenterExists.excenter_notMem_affineSpan_face, face_centroid_eq_iff, affineSpan_face_le, affineCombination_mem_interior_face_iff_mem_Ioo, face_restrict, affineCombination_mem_closedInterior_face_iff_nonneg, face_eq_mkOfPoint, face_centroid_eq_centroid, incenter_notMem_affineSpan_face, affineCombination_mem_setInterior_face_iff_mem, points_mem_affineSpan_face, range_face_points, mem_interior_face_iff_sbtw, face_points, orthogonalProjection_circumcenter, mem_closedInterior_face_iff_wbtw, affineCombination_mem_interior_face_iff_pos, range_face_reindex, closedInterior_face_eq_affineSegment, affineCombination_mem_closedInterior_face_iff_mem_Icc, face_points'
faceOpposite 📖	CompOp	60 math math: sSameSide_affineSpan_faceOpposite_point_left_iff, isTangentAt_insphere_iff_eq_touchpoint, faceOppositeCentroid_mem_affineSpan_face, wOppSide_affineSpan_faceOpposite_point_left_iff, sSameSide_excenter_singleton_point, ExcenterExists.excenter_notMem_affineSpan_faceOpposite, wSameSide_affineSpan_faceOpposite_iff, wOppSide_affineSpan_faceOpposite_point_right_iff, faceOpposite_map, sSameSide_incenter_point, ExcenterExists.touchpoint_notMem_affineSpan_of_ne, touchpoint_singleton_mem_interior_faceOpposite, isTangentAt_insphere_touchpoint, ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, affineSpan_faceOpposite_eq_orthRadius_insphere, ExcenterExists.isTangentAt_touchpoint, wSameSide_affineSpan_faceOpposite_point_left_iff, signedInfDist_apply_self, wOppSide_affineSpan_faceOpposite_iff, ExcenterExists.sOppSide_excenter_point_iff, wSameSide_affineSpan_faceOpposite_point_right_iff, points_mem_affineSpan_faceOpposite, faceOpposite_point_eq_point_zero, faceOpposite_restrict, affineSpan_faceOpposite_le, exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite, touchpoint_mem_affineSpan, range_faceOpposite_reindex, EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior, sOppSide_excenter_singleton_point, ExcenterExists.sOppSide_point_excenter_iff, sSameSide_affineSpan_faceOpposite_iff, sSameSide_affineSpan_faceOpposite_of_sign_eq, orthogonalProjectionSpan_faceOpposite_eq_point_rev, ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, sOppSide_point_excenter_singleton, affineCombination_mem_affineSpan_faceOpposite_iff, faceOpposite_point_eq_point_rev, faceOpposite_point_eq_point_succAbove, sOppSide_affineSpan_faceOpposite_of_pos_of_neg, points_notMem_affineSpan_faceOpposite, sSameSide_affineSpan_faceOpposite_point_right_iff, abs_signedInfDist_eq_dist_of_mem_affineSpan_range, touchpoint_empty_notMem_affineSpan_of_ne, sSameSide_point_excenter_singleton, orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, signedInfDist_affineCombination, sOppSide_affineSpan_faceOpposite_point_right_iff, faceOpposite_point_eq_point_one, altitudeFoot_mem_affineSpan_faceOpposite, sOppSide_affineSpan_faceOpposite_iff, range_faceOpposite_points, incenter_notMem_affineSpan_faceOpposite, touchpoint_empty_mem_interior_faceOpposite, ExcenterExists.sSameSide_excenter_point_iff, sSameSide_point_incenter, Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq, ExcenterExists.sSameSide_point_excenter_iff, sOppSide_affineSpan_faceOpposite_point_left_iff
instInhabitedOfNatNat 📖	CompOp	—
interior 📖	CompOp	16 math math: interior_subset_closedInterior, touchpoint_singleton_mem_interior_faceOpposite, interior_eq_empty, affineCombination_mem_interior_face_iff_mem_Ioo, interior_restrict, incenter_mem_interior, interior_map, mem_interior_face_iff_sbtw, point_notMem_interior, affineCombination_mem_interior_iff, interior_ssubset_closedInterior, affineCombination_mem_interior_face_iff_pos, interior_reindex, interior_eq_image_Ioo, touchpoint_empty_mem_interior_faceOpposite, mem_interior_iff_sbtw
map 📖	CompOp	36 math math: face_map, orthogonalProjectionSpan_map, circumcenter_map, incenter_map, restrict_map_restrict, faceOpposite_map, map_id, ExcenterExists.touchpoint_map, ExcenterExists.excenter_map, reindex_map, centroid_map, excenterWeightsUnnorm_map, exradius_map, altitudeFoot_map, interior_map, excenterExists_map, median_map, height_map, map_comp, map_mkOfPoint, excenterWeights_map, ExcenterExists.touchpointWeights_map, closedInterior_map, mongePoint_map, eulerPoint_map, setInterior_map, altitude_map, faceOppositeCentroid_map, ninePointCircle_map, inradius_map, map_subtype_restrict, restrict_map_subtype, restrict_map_inclusion, medial_map, map_points, circumradius_map
mkOfPoint 📖	CompOp	4 math math: range_mkOfPoint_points, face_eq_mkOfPoint, mkOfPoint_points, map_mkOfPoint
points 📖	CompOp	274 math math: sSameSide_affineSpan_faceOpposite_point_left_iff, isTangentAt_insphere_iff_eq_touchpoint, Affine.Triangle.equilateral_iff_dist_01_eq_02_and_dist_01_eq_12, affineCombination_mem_closedInterior_iff, altitudeFoot_restrict, faceOppositeCentroid_mem_affineSpan_face, wOppSide_affineSpan_faceOpposite_point_left_iff, Affine.Triangle.oangle_excenter_singleton_eq_add_pi, orthogonalProjectionSpan_map, faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, ExcenterExists.excenter_notMem_affineSpan_face, smul_mongePoint_vsub_circumcenter_eq_sum_vsub, sSameSide_excenter_singleton_point, neg_mul_lt_inner_vsub_altitudeFoot, Affine.Triangle.oangle_incenter_eq, smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point, orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan, inv_height_eq_sum_mul_inv_dist, ExcenterExists.excenter_notMem_affineSpan_faceOpposite, circumcenter_mem_affineSpan, affineSpan_pair_altitudeFoot_eq_altitude, restrict_reindex, excenter_singleton_mem_affineSpan_range, faceOppositeCentroid_restrict, dist_point_faceOppositeCentroid, face_centroid_eq_iff, Affine.Triangle.sSameSide_affineSpan_pair_point_incenter, centroid_eq_smul_sum_vsub_vadd, Affine.Triangle.sbtw_touchpoint_singleton, Affine.Triangle.dist_point_faceOppositeCentroid, mem_circumsphere, restrict_map_restrict, point_mem_median, Affine.Triangle.prod_dist_div_dist_eq_one_of_mem_line_of_mem_line, wSameSide_affineSpan_faceOpposite_iff, wOppSide_affineSpan_faceOpposite_point_right_iff, median_eq_line_point_centroid, ExcenterExists.affineCombination_eq_excenter_iff, univ_centroid_eq, affineIndependent_points_update_centroid, Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter, point_vsub_faceOppositeCentroid_eq_smul_vsub, orthogonalProjectionSpan_eq_point, centroid_eq_of_range_eq, sSameSide_incenter_point, affineSpan_face_le, circumradius_restrict, ExcenterExists.touchpoint_notMem_affineSpan_of_ne, abs_inner_vsub_altitudeFoot_div_lt_one, medial_restrict, centroid_weighted_vsub_eq_zero, Polygon.toTriangle_points, excenter_eq_affineCombination, Affine.Triangle.dist_div_sin_angle_eq_two_mul_circumradius, altitudeFoot_mem_affineSpan_image_compl, range_mkOfPoint_points, isTangentAt_insphere_touchpoint, ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, inner_mongePoint_vsub_face_centroid_vsub, ninePointCircle_restrict, affineCombination_mem_interior_face_iff_mem_Ioo, face_restrict, interior_restrict, affineSpan_faceOpposite_eq_orthRadius_insphere, dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, affineCombination_mem_closedInterior_face_iff_nonneg, Affine.Triangle.touchpoint_singleton_sbtw, face_eq_mkOfPoint, face_centroid_eq_centroid, Affine.Triangle.dist_circumcenter_reflection_orthocenter, abs_inner_vsub_altitudeFoot_lt_mul, ExcenterExists.isTangentAt_touchpoint, wSameSide_affineSpan_faceOpposite_point_left_iff, circumcenter_eq_point, altitude_restrict_eq_comap_subtype, signedInfDist_apply_self, centroid_notMem_affineSpan_of_ne_univ, wOppSide_affineSpan_faceOpposite_iff, ExcenterExists.sOppSide_excenter_point_iff, incenter_notMem_affineSpan_face, Affine.Triangle.affineSpan_pair_eq_orthRadius, orthogonalProjectionSpan_congr, mongePlane_def, Affine.Triangle.acuteAngled_iff_angle_lt, wSameSide_affineSpan_faceOpposite_point_right_iff, Affine.Triangle.toPolygon_vertices, altitudeFoot_eq_point_rev, vectorSpan_isOrtho_altitude_direction, mkOfPoint_points, altitudeFoot_mem_affineSpan, ExcenterExists.touchpointWeights_restrict, EuclideanGeometry.exists_of_range_subset_orthocentricSystem, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, affineCombination_mem_setInterior_face_iff_mem, Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point, ExcenterExists.excenter_restrict, points_mem_affineSpan_face, range_face_points, points_mem_affineSpan_faceOpposite, mem_interior_face_iff_sbtw, circumsphere_unique_dist_eq, faceOpposite_point_eq_point_zero, face_points, Affine.Triangle.two_zsmul_oangle_excenter_eq, Affine.Triangle.dist_orthocenter_reflection_circumcenter, map_altitude_restrict, faceOpposite_restrict, closedInterior_eq_affineSegment, point_notMem_interior, Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius, exradius_restrict, orthogonalProjection_circumcenter, affineSpan_faceOpposite_le, Affine.Triangle.prod_dist_eq_prod_dist_of_mem_line_of_mem_line, Affine.Triangle.orthocenter_replace_orthocenter_eq_point, mem_closedInterior_face_iff_wbtw, exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, smul_faceOppositeCentroid_vsub_point_eq_sum_vsub, orthogonalProjection_eq_circumcenter_of_exists_dist_eq, EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite, touchpoint_mem_affineSpan, affineCombination_mem_interior_iff, direction_mongePlane, dist_point_centroid, range_faceOpposite_reindex, affineCombination_eq_touchpoint_iff, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior, circumcenter_restrict, height_restrict, Affine.Triangle.affineSpan_orthocenter_point_le_altitude, point_vsub_faceOppositeCentroid_eq_smul_sum_vsub, sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair, faceOppositeCentroid_vsub_point_eq_smul_vsub, sOppSide_excenter_singleton_point, ExcenterExists.sOppSide_point_excenter_iff, mem_affineSpan_image_iff, dist_circumcenter_eq_circumradius, faceOppositeCentroid_eq_sum_vsub_vadd, EuclideanGeometry.eq_or_eq_reflection_of_dist_eq, incenter_restrict, Affine.Triangle.oangle_excenter_singleton_eq, inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero, sSameSide_affineSpan_faceOpposite_iff, sSameSide_affineSpan_faceOpposite_of_sign_eq, dist_circumcenter_eq_circumradius', orthogonalProjectionSpan_faceOpposite_eq_point_rev, EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter, affineCombination_mem_interior_face_iff_pos, ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, centroid_eq_smul_vsub_vadd_point, ExcenterExists.excenter_notMem_affineSpan_pair, pointsWithCircumcenter_point, inradius_restrict, Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere, mongePoint_eq_smul_vsub_vadd_circumcenter, centroid_vsub_faceOppositeCentroid_eq_smul_vsub, span_eq_top, incenter_eq_affineCombination, centroid_restrict, sOppSide_point_excenter_singleton, ninePointCircle_center_mem_affineSpan, eq_centroid_iff_sum_vsub_eq_zero, affineCombination_mem_affineSpan_faceOpposite_iff, orthogonalProjectionSpan_restrict, faceOpposite_point_eq_point_rev, mem_closedInterior_iff_wbtw, faceOpposite_point_eq_point_succAbove, setInterior_restrict, ExcenterExists.excenter_mem_affineSpan_range, excenterWeights_restrict, sOppSide_affineSpan_faceOpposite_of_pos_of_neg, Affine.Triangle.eulerPoint_eq_midpoint, reindex_points, range_face_reindex, medial_points, affineSpan_range_medial, median_restrict, points_notMem_affineSpan_faceOpposite, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, collinear_point_centroid_faceOppositeCentroid, point_eq_affineCombination_of_pointsWithCircumcenter, Equilateral.dist_eq, closedInterior_restrict, EuclideanGeometry.OrthocentricSystem.eq_insert_orthocenter, incenter_mem_affineSpan_range, sum_inv_height_sq_smul_vsub_eq_zero, closedInterior_face_eq_affineSegment, orthogonalProjection_eq_circumcenter_of_dist_eq, centroid_eq_iff, incenter_notMem_affineSpan_pair, mongePoint_restrict, touchpoint_eq_point_rev, eulerPoint_restrict, neg_one_lt_inner_vsub_altitudeFoot_div, centroid_eq_affineCombination, ExcenterExists.touchpoint_restrict, Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton, coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, sSameSide_affineSpan_faceOpposite_point_right_iff, excenterWeightsUnnorm_restrict, affineCombination_touchpointWeights, Affine.Triangle.orthocenter_mem_affineSpan, mongePoint_mem_affineSpan, smul_centroid_vsub_point_eq_sum_vsub, mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, point_vsub_centroid_eq_smul_vsub, faceOppositeCentroid_eq_smul_vsub_vadd_point, abs_signedInfDist_eq_dist_of_mem_affineSpan_range, affineCombination_mem_closedInterior_face_iff_mem_Icc, orthogonalProjectionSpan_reindex, Affine.Triangle.sbtw_touchpoint_empty, independent, touchpoint_empty_notMem_affineSpan_of_ne, faceOppositeCentroid_vsub_centroid_eq_smul_vsub, sSameSide_point_excenter_singleton, mem_altitude, Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton, Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius, orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, height_eq_dist, reindex_range_points, signedInfDist_affineCombination, sOppSide_affineSpan_faceOpposite_point_right_iff, faceOppositeCentroid_vsub_faceOppositeCentroid, faceOpposite_point_eq_point_one, setInterior_subset_affineSpan, touchpoint_mem_affineSpan_simplex, point_mem_closedInterior, Equilateral.angle_eq_pi_div_three, ext_iff, Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point, interior_eq_image_Ioo, Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius, face_points', reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, map_subtype_restrict, restrict_map_subtype, Affine.Triangle.orthocenter_vsub_circumcenter_eq_sum_vsub, affineCombination_mem_setInterior_iff, altitudeFoot_mem_affineSpan_faceOpposite, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, affineSpan_pair_eq_altitude_iff, closedInterior_subset_affineSpan, signedInfDist_apply_of_ne, direction_altitude, restrict_map_inclusion, circumcenter_eq_centroid, convexHull_eq_closedInterior, sOppSide_affineSpan_faceOpposite_iff, range_faceOpposite_points, Affine.Triangle.sSameSide_affineSpan_pair_incenter_point, centroid_eq_affineCombination_of_pointsWithCircumcenter, incenter_notMem_affineSpan_faceOpposite, faceOppositeCentroid_eq_affineCombination, centroid_mem_affineSpan, closedInterior_eq_singleton, centroid_vsub_point_eq_smul_vsub, points_vsub_eulerPoint, ExcenterExists.sSameSide_excenter_point_iff, centroid_vsub_eq, map_points, Affine.Triangle.dist_point_centroid, altitude_def, restrict_points_coe, mem_interior_iff_sbtw, excenterExists_restrict, Affine.Triangle.equilateral_iff_dist_eq_and_dist_eq, sSameSide_point_incenter, Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq, ExcenterExists.sSameSide_point_excenter_iff, sOppSide_affineSpan_faceOpposite_point_left_iff, inner_vsub_vsub_altitudeFoot_eq_height_sq
reindex 📖	CompOp	45 math math: restrict_reindex, medial_reindex, excenterWeightsUnnorm_reindex, reindex_map, excenterExists_reindex, circumcenter_reindex, scalene_reindex_iff, equilateral_reindex_iff, excenterWeights_reindex, inradius_reindex, median_reindex, exsphere_reindex, reindex_trans, exradius_reindex, ninePointCircle_reindex, touchpointWeights_reindex, range_faceOpposite_reindex, altitudeFoot_reindex, mongePoint_reindex, altitude_reindex, faceOppositeCentroid_reindex, regular_reindex_iff, touchpoint_reindex, interior_reindex, reindex_points, range_face_reindex, eulerPoint_reindex, signedInfDist_reindex, incenter_reindex, orthogonalProjectionSpan_reindex, acuteAngled_reindex_iff, mongePlane_reindex, reindex_range_points, circumsphere_reindex, circumradius_reindex, centroid_reindex, height_reindex, reindex_refl, excenter_reindex, reindex_symm_reindex, closedInterior_reindex, setInterior_reindex, reindex_reindex_symm, Affine.Triangle.orthocenter_reindex, insphere_reindex
restrict 📖	CompOp	34 math math: altitudeFoot_restrict, restrict_reindex, faceOppositeCentroid_restrict, restrict_map_restrict, circumradius_restrict, medial_restrict, ninePointCircle_restrict, face_restrict, interior_restrict, altitude_restrict_eq_comap_subtype, ExcenterExists.touchpointWeights_restrict, ExcenterExists.excenter_restrict, map_altitude_restrict, faceOpposite_restrict, exradius_restrict, circumcenter_restrict, height_restrict, incenter_restrict, inradius_restrict, centroid_restrict, orthogonalProjectionSpan_restrict, setInterior_restrict, excenterWeights_restrict, median_restrict, closedInterior_restrict, mongePoint_restrict, eulerPoint_restrict, ExcenterExists.touchpoint_restrict, excenterWeightsUnnorm_restrict, map_subtype_restrict, restrict_map_subtype, restrict_map_inclusion, restrict_points_coe, excenterExists_restrict
setInterior 📖	CompOp	7 math math: affineCombination_mem_setInterior_face_iff_mem, setInterior_mono, setInterior_restrict, setInterior_map, setInterior_subset_affineSpan, affineCombination_mem_setInterior_iff, setInterior_reindex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineCombination_mem_affineSpan_faceOpposite_iff 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan independent range_faceOpposite_points Finset.mem_univ subsingleton_or_nontrivial Module.subsingleton AddTorsor.subsingleton_iff affineSpan_eq_top_iff_nonempty_of_subsingleton Fin.instNontrivial Nat.instAtLeastTwoHAddOfNat affineCombination_mem_affineSpan_image
affineCombination_mem_closedInterior_face_iff_mem_Icc 📖	mathematical	Finset.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership closedInterior face DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	affineCombination_mem_setInterior_face_iff_mem
affineCombination_mem_closedInterior_face_iff_nonneg 📖	mathematical	Finset.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership closedInterior face DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	affineCombination_mem_closedInterior_face_iff_mem_Icc Finset.sum_subset Finset.subset_univ Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono
affineCombination_mem_closedInterior_iff 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership closedInterior DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	affineCombination_mem_setInterior_iff
affineCombination_mem_interior_face_iff_mem_Ioo 📖	mathematical	Finset.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership interior face DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	affineCombination_mem_setInterior_face_iff_mem
affineCombination_mem_interior_face_iff_pos 📖	mathematical	Finset.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership interior face DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	affineCombination_mem_interior_face_iff_mem_Ioo Finset.sum_subset Finset.subset_univ Finset.exists_mem_ne Finset.single_lt_sum IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono LT.lt.le
affineCombination_mem_interior_iff 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership interior DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	affineCombination_mem_setInterior_iff
affineCombination_mem_setInterior_face_iff_mem 📖	mathematical	Finset.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership setInterior face DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	eq_affineCombination_of_mem_affineSpan_of_fintype Set.mem_of_mem_of_subset setInterior_subset_affineSpan AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype independent Finset.range_orderEmbOfFin Set.indicator_of_mem Finset.mem_coe Function.Injective.extend_apply RelEmbedding.injective affineCombination_mem_setInterior_iff Set.indicator_of_notMem Fintype.sum_of_injective Finset.map_orderEmbOfFin_univ Finset.affineCombination_indicator_subset Finset.subset_univ Finset.affineCombination_map
affineCombination_mem_setInterior_iff 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Set Set.instMembership setInterior DFunLike.coe AffineMap Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall AffineMap.instFunLike Finset.affineCombination Finset.univ Fin.fintype points	—	affineIndependent_iff_eq_of_fintype_affineCombination_eq independent
affineSpan_faceOpposite_le 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points faceOpposite	—	affineSpan_face_le
affineSpan_face_le 📖	mathematical	Finset.card	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points face	—	affineSpan_mono Set.image_subset_range range_face_points
closedInterior_eq_singleton 📖	mathematical	—	closedInterior Set Set.instSingletonSet points	—	Set.ext Finset.sum_congr Finset.univ_unique Finset.sum_singleton AddTorsor.nonempty Finset.weightedVSubOfPoint_apply one_smul vsub_vadd instReflLe
closedInterior_map 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	closedInterior map Set.image DFunLike.coe AffineMap AffineMap.instFunLike	—	setInterior_map
closedInterior_reindex 📖	mathematical	—	closedInterior reindex	—	setInterior_reindex
closedInterior_restrict 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	closedInterior Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range points DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict Set.preimage AffineSubspace.subtype	—	setInterior_restrict
closedInterior_subset_affineSpan 📖	mathematical	—	Set Set.instHasSubset closedInterior SetLike.coe AffineSubspace AffineSubspace.instSetLike affineSpan Set.range points	—	affineCombination_mem_affineSpan_of_nonempty
ext 📖	—	points	—	—	—
ext_iff 📖	mathematical	—	points	—	ext
faceOpposite_map 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	faceOpposite map	—	—
faceOpposite_point_eq_point_one 📖	mathematical	—	points faceOpposite	—	faceOpposite_point_eq_point_rev
faceOpposite_point_eq_point_rev 📖	mathematical	—	points faceOpposite	—	faceOpposite_point_eq_point_succAbove
faceOpposite_point_eq_point_succAbove 📖	mathematical	—	points faceOpposite Fin.succAbove MulZeroClass.toZero Nat.instMulZeroClass	—	Finset.orderEmbOfFin_compl_singleton_apply
faceOpposite_point_eq_point_zero 📖	mathematical	—	points faceOpposite	—	faceOpposite_point_eq_point_rev
faceOpposite_restrict 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	faceOpposite Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range points DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict LE.le.trans PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan_faceOpposite_le	—	face_restrict
face_eq_mkOfPoint 📖	mathematical	—	face Finset Finset.instSingleton Finset.card_singleton mkOfPoint points	—	ext Finset.card_singleton Finset.orderEmbOfFin_singleton
face_map 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike Finset.card	face map	—	—
face_points 📖	mathematical	Finset.card	points face DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Fin.instLinearOrder instFunLikeOrderEmbedding Finset.orderEmbOfFin	—	—
face_points' 📖	mathematical	Finset.card	points face DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Fin.instLinearOrder instFunLikeOrderEmbedding Finset.orderEmbOfFin	—	—
face_restrict 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points Finset.card	face Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range points DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict LE.le.trans PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan_face_le	—	ext Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange LE.le.trans affineSpan_face_le restrict_points_coe
independent 📖	mathematical	—	AffineIndependent points	—	—
instNonemptyElemComplSetSingletonOfNontrivial 📖	mathematical	—	Set.Elem Compl.compl Set Set.instCompl Set.instSingletonSet	—	Set.Nonempty.to_subtype Set.nonempty_compl_of_nontrivial
interior_eq_empty 📖	mathematical	—	interior Set Set.instEmptyCollection	—	Set.ext Finset.sum_congr Finset.univ_unique Finset.sum_singleton
interior_map 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	interior map Set.image DFunLike.coe AffineMap AffineMap.instFunLike	—	setInterior_map
interior_reindex 📖	mathematical	—	interior reindex	—	setInterior_reindex
interior_restrict 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	interior Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range points DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict Set.preimage AffineSubspace.subtype	—	setInterior_restrict
interior_ssubset_closedInterior 📖	mathematical	—	Set Set.instHasSSubset interior closedInterior	—	Set.ssubset_iff_exists interior_subset_closedInterior point_mem_closedInterior point_notMem_interior
interior_subset_closedInterior 📖	mathematical	—	Set Set.instHasSubset interior closedInterior	—	LT.lt.le
map_comp 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	map AffineMap.comp DFunLike.coe AffineMap AffineMap.instFunLike	—	ext
map_id 📖	mathematical	—	map AffineMap.id	—	ext
map_mkOfPoint 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	map mkOfPoint DFunLike.coe AffineMap AffineMap.instFunLike	—	—
map_points 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	points map DFunLike.coe AffineMap AffineMap.instFunLike	—	—
map_subtype_restrict 📖	mathematical	—	restrict map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor AffineSubspace.subtype Subtype.coe_injective Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points Set Set.instHasSubset SetLike.coe affineSpan_le	—	Nonempty.map Subtype.coe_injective instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange affineSpan_le
mem_affineSpan_image_iff 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.image points Set Set.instMembership	—	AffineIndependent.mem_affineSpan_iff independent
mkOfPoint_points 📖	mathematical	—	points mkOfPoint	—	—
nonempty 📖	mathematical	—	Affine.Simplex	—	AddTorsor.nonempty
point_mem_closedInterior 📖	mathematical	—	Set Set.instMembership closedInterior points	—	Finset.affineCombination_affineCombinationSingleWeights Finset.mem_univ affineCombination_mem_closedInterior_iff Finset.sum_affineCombinationSingleWeights Finset.affineCombinationSingleWeights.congr_simp Finset.affineCombinationSingleWeights_apply_self instReflLe Finset.affineCombinationSingleWeights_apply_of_ne
point_notMem_interior 📖	mathematical	—	Set Set.instMembership interior points	—	Finset.affineCombination_affineCombinationSingleWeights Finset.mem_univ affineCombination_mem_interior_iff Finset.sum_affineCombinationSingleWeights Finset.affineCombinationSingleWeights_apply_self
points_mem_affineSpan_face 📖	mathematical	Finset.card	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points face Finset Finset.instSetLike	—	range_face_points AffineIndependent.mem_affineSpan_iff independent
points_mem_affineSpan_faceOpposite 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite	—	faceOpposite.eq_1 points_mem_affineSpan_face
points_notMem_affineSpan_faceOpposite 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set.range points faceOpposite	—	points_mem_affineSpan_faceOpposite
range_faceOpposite_points 📖	mathematical	—	Set.range points faceOpposite Set.image Compl.compl Set Set.instCompl Set.instSingletonSet	—	range_face_points Finset.coe_compl Finset.coe_singleton
range_faceOpposite_reindex 📖	mathematical	—	Set.range points faceOpposite reindex DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	faceOpposite.eq_1 Finset.card_map range_face_reindex range_face_points Finset.coe_map Set.image_congr Finset.coe_compl Finset.coe_singleton Equiv.image_compl Set.image_singleton range_faceOpposite_points
range_face_points 📖	mathematical	Finset.card	Set.range points face Set.image SetLike.coe Finset Finset.instSetLike	—	face_points' Set.range_comp Finset.range_orderEmbOfFin
range_face_reindex 📖	mathematical	Finset.card	Set.range points face reindex Finset.map Equiv.toEmbedding Equiv.symm Finset.card Finset.card_map	—	Finset.card_map range_face_points Set.image_congr Set.image_comp Finset.coe_map
range_mkOfPoint_points 📖	mathematical	—	Set.range points mkOfPoint Set Set.instSingletonSet	—	—
reindex_map 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	reindex map	—	—
reindex_points 📖	mathematical	—	points reindex DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—
reindex_range_points 📖	mathematical	—	Set.range points reindex	—	reindex.eq_1 Set.range_comp Equiv.range_eq_univ Set.image_univ
reindex_refl 📖	mathematical	—	reindex Equiv.refl	—	ext
reindex_reindex_symm 📖	mathematical	—	reindex Equiv.symm	—	reindex_trans Equiv.self_trans_symm reindex_refl
reindex_symm_reindex 📖	mathematical	—	reindex Equiv.symm	—	reindex_trans Equiv.symm_trans_self reindex_refl
reindex_trans 📖	mathematical	—	reindex Equiv.trans	—	—
restrict_map_inclusion 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range points DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict Set.inclusion_injective LE.le.trans PartialOrder.toPreorder AffineSubspace.instPartialOrder	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.inclusion_injective
restrict_map_restrict 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points AffineSubspace.map	map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range points DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion AffineSubspace.map AffineSubspace.nonempty_map restrict AffineMap.restrict AffineMap.restrict.injective LE.le.trans PartialOrder.toPreorder AffineSubspace.instPartialOrder Eq.trans_le Preorder.toLE AffineSubspace.map_mono	—	Nonempty.map AffineSubspace.nonempty_map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange AffineMap.restrict.injective
restrict_map_subtype 📖	mathematical	—	map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction affineSpan Set.range points AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion le_rfl PartialOrder.toPreorder AffineSubspace.instPartialOrder AffineMap.instFunLike AffineSubspace.inclusion restrict AffineSubspace.subtype Subtype.coe_injective	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange le_rfl Subtype.coe_injective
restrict_points_coe 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike points Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange
restrict_reindex 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	restrict reindex Set Set.range points AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan reindex_range_points Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange reindex_range_points
setInterior_map 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	setInterior map Set.image DFunLike.coe AffineMap AffineMap.instFunLike	—	Set.ext Set.mem_image eq_affineCombination_of_mem_affineSpan_of_fintype affineCombination_mem_setInterior_iff map_points Finset.map_affineCombination Set.mem_of_mem_of_subset setInterior_subset_affineSpan Mathlib.Tactic.Contrapose.contrapose₄ Set.range_comp AffineSubspace.map_span AffineSubspace.mem_map
setInterior_mono 📖	mathematical	Set Set.instHasSubset	Set Set.instHasSubset setInterior	—	—
setInterior_reindex 📖	mathematical	—	setInterior reindex	—	Set.ext Equiv.self_comp_symm Function.comp_assoc Equiv.coe_toEmbedding Finset.affineCombination_map Finset.map_univ_equiv Finset.sum_comp_equiv affineCombination_mem_setInterior_iff Equiv.symm_comp_self
setInterior_restrict 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder affineSpan Set.range points	setInterior Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor Nonempty.map affineSpan Set.range points DFunLike.coe AffineMap instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike AffineSubspace.inclusion restrict Set.preimage AffineSubspace.subtype	—	Nonempty.map instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.instNonemptyRange Function.Injective.image_injective AffineSubspace.subtype_injective Set.image_preimage_eq_of_subset HasSubset.Subset.trans Set.instIsTransSubset setInterior_subset_affineSpan Subtype.range_coe_subtype setInterior_map
setInterior_subset_affineSpan 📖	mathematical	—	Set Set.instHasSubset setInterior SetLike.coe AffineSubspace AffineSubspace.instSetLike affineSpan Set.range points	—	affineCombination_mem_affineSpan_of_nonempty

---

← Back to Index