Basic

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

Statistics

Metric	Count
Definitions «term_∥_», ofEq, comap, gciMapComap, inclusion, map, subtype, toAddTorsor, topEquiv, unique_affineSpan_singleton	10
Theorems coe_ofEq_apply, ext_on, linear_ofEq, ofEq_rfl, ofEq_symm, span_eq_top_iff, eqOn_affineSpan, ext_on, lineMap_mem, lineMap_mem_affineSpan_pair, lineMap_rev_mem_affineSpan_pair, linear_eqOn_vectorSpan, map_top_of_surjective, map_vectorSpan, span_eq_top_of_surjective, vectorSpan_image_eq_submodule_map, direction_eq, refl, trans, vectorSpan_eq, affineSpan_pair_comm, affineSpan_pair_parallel_iff_exists_unit_smul, affineSpan_pair_parallel_iff_exists_unit_smul', affineSpan_pair_parallel_iff_vectorSpan_eq, affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, bot_parallel_iff_eq_bot, coe_affineSpan_singleton, coe_comap, coe_inclusion_apply, coe_map, coe_subtype, coe_vadd, coe_vsub, comap_bot, comap_comap, comap_id, comap_inf, comap_map_eq_of_injective, comap_mono, comap_span, comap_supr, comap_symm, comap_top, direction_affineSpan_insert, direction_affineSpan_pair_le_iff_exists_smul, direction_lt_of_nonempty, direction_sup, direction_sup_eq_sup_direction, eq_univ_of_subsingleton_span_eq_top, gc_map_comap, inclusion_linear, inclusion_rfl, le_comap_map, linear_topEquiv, map_bot, map_comap_le, map_direction, map_eq_bot_iff, map_iSup, map_id, map_inf_eq, map_inf_le, map_le_iff_le_comap, map_map, map_mk', map_mono, map_span, map_sup, map_symm, mem_affineSpan_insert_iff, mem_affineSpan_singleton, mem_comap, mem_map, mem_map_iff_mem_of_injective, mem_map_of_mem, parallel_bot_iff_eq_bot, parallel_comm, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, preimage_coe_affineSpan_singleton, subsingleton_of_subsingleton_span_eq_top, subtype_apply, subtype_injective, subtype_linear, topEquiv_apply, topEquiv_symm_apply_coe, vectorSpan_union_of_mem_of_mem, vsub_left_mem_direction_iff_mem, vsub_right_mem_direction_iff_mem, affineSpan_coe_preimage_eq_top, affineSpan_pair_eq_of_left_mem_of_ne, affineSpan_pair_eq_of_mem_of_mem_of_ne, affineSpan_pair_eq_of_right_mem_of_ne, affineSpan_singleton_union_vadd_eq_top_of_span_eq_top, exists_eq_smul_of_parallel, mem_affineSpan_pair_iff_exists_lineMap_eq, mem_affineSpan_pair_iff_exists_lineMap_rev_eq, mem_vectorSpan_pair, mem_vectorSpan_pair_rev, smul_vsub_rev_vadd_mem_affineSpan_pair, smul_vsub_vadd_mem_affineSpan_pair, vadd_left_mem_affineSpan_pair, vadd_right_mem_affineSpan_pair, vectorSpan_eq_span_vsub_finset_right_ne, vectorSpan_eq_span_vsub_set_left, vectorSpan_eq_span_vsub_set_left_ne, vectorSpan_eq_span_vsub_set_right, vectorSpan_eq_span_vsub_set_right_ne, vectorSpan_image_eq_span_vsub_set_left_ne, vectorSpan_image_eq_span_vsub_set_right_ne, vectorSpan_pair, vectorSpan_pair_rev, vectorSpan_range_eq_span_range_vsub_left, vectorSpan_range_eq_span_range_vsub_left_ne, vectorSpan_range_eq_span_range_vsub_right, vectorSpan_range_eq_span_range_vsub_right_ne, vectorSpan_vadd	116
Total	126

Affine

Definitions

Name	Category	Theorems
«term_∥_» 📖	CompOp	—

AffineEquiv

Definitions

Name	Category	Theorems
ofEq 📖	CompOp	4 math math: linear_ofEq, ofEq_symm, coe_ofEq_apply, ofEq_rfl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ofEq_apply 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe AffineEquiv Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor EquivLike.toFunLike equivLike ofEq	—	—
ext_on 📖	—	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.EqOn DFunLike.coe AffineEquiv EquivLike.toFunLike equivLike	—	—	AffineMap.ext_on
linear_ofEq 📖	mathematical	—	linear AffineSubspace SetLike.instMembership AffineSubspace.instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor ofEq LinearEquiv.ofEq	—	RingHomInvPair.ids
ofEq_rfl 📖	mathematical	—	ofEq AffineSubspace refl SetLike.instMembership AffineSubspace.instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor	—	—
ofEq_symm 📖	mathematical	—	symm AffineSubspace SetLike.instMembership AffineSubspace.instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor ofEq	—	ext
span_eq_top_iff 📖	mathematical	—	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.image DFunLike.coe AffineEquiv EquivLike.toFunLike equivLike	—	AffineMap.span_eq_top_of_surjective surjective Set.image_comp Set.image_congr symm_apply_apply Set.image_id'

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_affineSpan 📖	mathematical	Set.EqOn DFunLike.coe AffineMap instFunLike	SetLike.coe AffineSubspace AffineSubspace.instSetLike affineSpan	—	Set.eq_empty_or_nonempty AffineSubspace.span_empty map_vadd linear_eqOn_vectorSpan
ext_on 📖	—	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.EqOn DFunLike.coe AffineMap instFunLike	—	—	eqOn_affineSpan
lineMap_mem 📖	mathematical	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	lineMap_apply AffineSubspace.smul_vsub_vadd_mem
lineMap_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	lineMap_mem left_mem_affineSpan_pair right_mem_affineSpan_pair
lineMap_rev_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	lineMap_mem right_mem_affineSpan_pair left_mem_affineSpan_pair
linear_eqOn_vectorSpan 📖	mathematical	Set.EqOn DFunLike.coe AffineMap instFunLike	LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear SetLike.coe Submodule Submodule.setLike vectorSpan	—	LinearMap.eqOn_span linearMap_vsub
map_top_of_surjective 📖	mathematical	DFunLike.coe AffineMap instFunLike	AffineSubspace.map Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	AffineSubspace.ext_iff Set.image_univ_of_surjective
map_vectorSpan 📖	mathematical	—	Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids linear vectorSpan Set.image DFunLike.coe AffineMap instFunLike	—	RingHomSurjective.ids image_vsub_image Submodule.span_image
span_eq_top_of_surjective 📖	mathematical	DFunLike.coe AffineMap instFunLike affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Set.image	—	AffineSubspace.map_span map_top_of_surjective
vectorSpan_image_eq_submodule_map 📖	mathematical	—	Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids linear vectorSpan Set.image DFunLike.coe AffineMap instFunLike	—	map_vectorSpan

AffineSubspace

Definitions

Name	Category	Theorems
comap 📖	CompOp	18 math math: comap_bot, comap_symm, map_symm, Affine.Simplex.altitude_restrict_eq_comap_subtype, mem_comap, comap_map_eq_of_injective, map_comap_le, comap_span, gc_map_comap, comap_comap, map_le_iff_le_comap, comap_supr, le_comap_map, comap_top, comap_id, comap_mono, coe_comap, comap_inf
gciMapComap 📖	CompOp	—
inclusion 📖	CompOp	36 math math: Affine.Simplex.altitudeFoot_restrict, Affine.Simplex.restrict_reindex, Affine.Simplex.faceOppositeCentroid_restrict, Affine.Simplex.restrict_map_restrict, Affine.Simplex.circumradius_restrict, Affine.Simplex.medial_restrict, Affine.Simplex.ninePointCircle_restrict, Affine.Simplex.face_restrict, Affine.Simplex.interior_restrict, inclusion_linear, Affine.Simplex.altitude_restrict_eq_comap_subtype, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, Affine.Simplex.ExcenterExists.excenter_restrict, Affine.Simplex.map_altitude_restrict, Affine.Simplex.faceOpposite_restrict, Affine.Simplex.exradius_restrict, Affine.Simplex.circumcenter_restrict, Affine.Simplex.height_restrict, Affine.Simplex.incenter_restrict, Affine.Simplex.inradius_restrict, Affine.Simplex.centroid_restrict, Affine.Simplex.orthogonalProjectionSpan_restrict, Affine.Simplex.setInterior_restrict, Affine.Simplex.excenterWeights_restrict, Affine.Simplex.median_restrict, Affine.Simplex.closedInterior_restrict, Affine.Simplex.mongePoint_restrict, Affine.Simplex.eulerPoint_restrict, coe_inclusion_apply, Affine.Simplex.ExcenterExists.touchpoint_restrict, Affine.Simplex.excenterWeightsUnnorm_restrict, inclusion_rfl, Affine.Simplex.restrict_map_subtype, Affine.Simplex.restrict_map_inclusion, Affine.Simplex.restrict_points_coe, Affine.Simplex.excenterExists_restrict
map 📖	CompOp	54 math math: AffineEquiv.sOppSide_map_iff, AffineMap.restrict.bijective, map_pointwise_vadd, EuclideanGeometry.reflection_map, EuclideanGeometry.orthogonalProjection_map, comap_symm, map_mk', AffineEquiv.sSameSide_map_iff, map_symm, finiteDimensional_direction_map, isometryEquivMap.toAffineMap_eq, map_inf_eq, EuclideanGeometry.orthogonalProjection_subtype, Affine.Simplex.map_altitude_restrict, Affine.Simplex.median_map, AffineEquiv.wSameSide_map_iff, mem_map, mem_map_iff_mem_of_injective, WSameSide.map, isometryEquivMap.coe_apply, map_span, Function.Injective.sSameSide_map_iff, AffineMap.map_top_of_surjective, comap_map_eq_of_injective, map_direction, Function.Injective.sOppSide_map_iff, smul_eq_map, map_comap_le, pointwise_vadd_eq_map, map_inf_le, map_map, gc_map_comap, linear_equivMapOfInjective, Affine.Simplex.median_restrict, map_bot, map_id, map_eq_bot_iff, EuclideanGeometry.Sphere.orthRadius_map, map_le_iff_le_comap, Affine.Simplex.altitude_map, WOppSide.map, le_comap_map, map_sup, AffineEquiv.wOppSide_map_iff, EuclideanGeometry.reflection_subtype, isometryEquivMap.apply_symm_apply, Function.Injective.wSameSide_map_iff, nonempty_map, equivMapOfInjective_toFun, map_iSup, map_mono, Function.Injective.wOppSide_map_iff, mem_map_of_mem, coe_map
subtype 📖	CompOp	17 math math: subtype_apply, coe_subtypeₐᵢ, Affine.Simplex.interior_restrict, Affine.Simplex.altitude_restrict_eq_comap_subtype, EuclideanGeometry.orthogonalProjection_subtype, Affine.Simplex.map_altitude_restrict, subtypeA_toAffineMap, subtype_injective, subtype_linear, Affine.Simplex.setInterior_restrict, Affine.Simplex.median_restrict, Affine.Simplex.closedInterior_restrict, coe_subtype, EuclideanGeometry.reflection_subtype, Affine.Simplex.map_subtype_restrict, Affine.Simplex.restrict_map_subtype, subtypeₐᵢ_toAffineMap
toAddTorsor 📖	CompOp	138 math math: Affine.Simplex.altitudeFoot_restrict, coe_vsub, Affine.Simplex.orthogonalProjectionSpan_map, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, AffineMap.restrict.bijective, Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Affine.Simplex.restrict_reindex, Affine.Simplex.faceOppositeCentroid_restrict, EuclideanGeometry.orthogonalProjection_congr, Affine.Simplex.restrict_map_restrict, EuclideanGeometry.orthogonalProjection_contLinear, EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq, coe_subtypeA, subtype_apply, EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection, EuclideanGeometry.inter_eq_singleton_orthogonalProjection, linear_topEquiv, Affine.Simplex.orthogonalProjectionSpan_eq_point, EuclideanGeometry.orthogonalProjection_map, 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, Affine.Simplex.ninePointCircle_restrict, Affine.Simplex.face_restrict, Affine.Simplex.interior_restrict, inclusion_linear, EuclideanGeometry.orthogonalProjection_apply', Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le, EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, 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, Affine.Simplex.orthogonalProjectionSpan_congr, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection, EuclideanGeometry.orthogonalProjection_subtype, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, Affine.Simplex.ExcenterExists.excenter_restrict, EuclideanGeometry.orthogonalProjection_vadd_eq_self, 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, Affine.Simplex.orthogonalProjection_circumcenter, subtypeA_toAffineMap, Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, coe_vadd, Affine.Simplex.circumcenter_restrict, AffineMap.restrict.injective, Affine.Simplex.height_restrict, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, subtype_injective, subtype_linear, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, topEquiv_symm_apply_coe, Affine.Simplex.incenter_restrict, EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, EuclideanGeometry.dist_orthogonalProjection_eq_infNndist, AffineMap.restrict.surjective, Affine.Simplex.inradius_restrict, AffineMap.restrict.coe_apply, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, Affine.Simplex.centroid_restrict, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, EuclideanGeometry.orthogonalProjection_mem, Affine.Simplex.orthogonalProjectionSpan_restrict, Affine.Simplex.setInterior_restrict, Affine.Simplex.excenterWeights_restrict, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, AffineEquiv.ofEq_symm, EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq, linear_equivMapOfInjective, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, Affine.Simplex.median_restrict, affineSpan_coe_preimage_eq_top, EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq, Affine.Simplex.closedInterior_restrict, EuclideanGeometry.orthogonalProjection_orthogonalProjection, EuclideanGeometry.orthogonalProjection_vsub_mem_direction, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, topEquiv_apply, Affine.Simplex.mongePoint_restrict, Affine.Simplex.eulerPoint_restrict, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, coe_inclusion_apply, Affine.Simplex.ExcenterExists.touchpoint_restrict, Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Affine.Simplex.excenterWeightsUnnorm_restrict, EuclideanGeometry.Sphere.IsTangent.isTangentAt, EuclideanGeometry.reflection_apply', EuclideanGeometry.oangle_self_orthogonalProjection, AffineEquiv.coe_ofEq_apply, AffineMap.restrict.linear, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, coe_subtype, Affine.Simplex.orthogonalProjectionSpan_reindex, EuclideanGeometry.orthogonalProjection_linear, signedInfDist_def, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, Affine.Simplex.signedInfDist_affineCombination, EuclideanGeometry.angle_self_orthogonalProjection, EuclideanGeometry.orthogonalProjection_eq_self_iff, EuclideanGeometry.reflection_subtype, inclusion_rfl, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal, EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace, EuclideanGeometry.orthogonalProjection_apply, signedInfDist_apply_self, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, EuclideanGeometry.orthogonalProjection_mem_orthogonal, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, equivMapOfInjective_toFun, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem, Affine.Simplex.map_subtype_restrict, Affine.Simplex.restrict_map_subtype, 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, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, AffineEquiv.ofEq_rfl, EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq, Affine.Simplex.restrict_points_coe, Affine.Simplex.excenterExists_restrict, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self
topEquiv 📖	CompOp	3 math math: linear_topEquiv, topEquiv_symm_apply_coe, topEquiv_apply
unique_affineSpan_singleton 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_pair_comm 📖	mathematical	—	affineSpan Set Set.instInsert Set.instSingletonSet	—	Set.pair_comm
affineSpan_pair_parallel_iff_exists_unit_smul 📖	mathematical	—	Parallel affineSpan Set Set.instInsert Set.instSingletonSet Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	affineSpan_pair_parallel_iff_exists_unit_smul' inv_smul_smul
affineSpan_pair_parallel_iff_exists_unit_smul' 📖	mathematical	—	Parallel affineSpan Set Set.instInsert Set.instSingletonSet Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	affineSpan_pair_parallel_iff_vectorSpan_eq vectorSpan_pair_rev Submodule.span_singleton_eq_span_singleton
affineSpan_pair_parallel_iff_vectorSpan_eq 📖	mathematical	—	Parallel affineSpan Set Set.instInsert Set.instSingletonSet vectorSpan	—	—
affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty 📖	mathematical	—	Parallel affineSpan vectorSpan Set Set.instEmptyCollection	—	direction_affineSpan affineSpan_eq_bot parallel_iff_direction_eq_and_eq_bot_iff_eq_bot
bot_parallel_iff_eq_bot 📖	mathematical	—	Parallel Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	parallel_comm parallel_bot_iff_eq_bot
coe_affineSpan_singleton 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike affineSpan Set Set.instSingletonSet	—	Set.ext mem_coe vsub_right_mem_direction_iff_mem mem_affineSpan Set.mem_singleton direction_affineSpan vectorSpan_singleton
coe_comap 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike comap Set.preimage DFunLike.coe AffineMap AffineMap.instFunLike	—	—
coe_inclusion_apply 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction Submodule.addCommGroup Submodule.module toAddTorsor Nonempty.map Set.Elem SetLike.coe Set.inclusion AffineMap.instFunLike inclusion	—	Nonempty.map
coe_map 📖	mathematical	—	SetLike.coe AffineSubspace instSetLike map Set.image DFunLike.coe AffineMap AffineMap.instFunLike	—	—
coe_subtype 📖	mathematical	—	DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction AffineSubspace instSetLike Submodule.addCommGroup Submodule.module toAddTorsor AffineMap.instFunLike subtype	—	—
coe_vadd 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike HVAdd.hVAdd Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.addCommGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction toAddTorsor	—	—
coe_vsub 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction VSub.vsub AffineSubspace instSetLike AddTorsor.toVSub AddCommGroup.toAddGroup Submodule.addCommGroup toAddTorsor	—	—
comap_bot 📖	mathematical	—	comap Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
comap_comap 📖	mathematical	—	comap AffineMap.comp	—	—
comap_id 📖	mathematical	—	comap AffineMap.id	—	—
comap_inf 📖	mathematical	—	comap AffineSubspace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.u_inf gc_map_comap
comap_map_eq_of_injective 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	comap map	—	GaloisCoinsertion.u_l_eq
comap_mono 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder	comap	—	Set.preimage_mono
comap_span 📖	mathematical	—	comap AffineEquiv.toAffineMap affineSpan Set.preimage DFunLike.coe AffineEquiv EquivLike.toFunLike AffineEquiv.equivLike	—	map_symm map_span AffineEquiv.coe_coe AffineEquiv.image_symm
comap_supr 📖	mathematical	—	comap iInf AffineSubspace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.u_iInf gc_map_comap
comap_symm 📖	mathematical	—	comap AffineEquiv.toAffineMap AffineEquiv.symm map	—	coe_injective AffineEquiv.preimage_symm
comap_top 📖	mathematical	—	comap Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext_iff Set.preimage_univ
direction_affineSpan_insert 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	direction affineSpan Set Set.instInsert SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.span Set.instSingletonSet VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	sup_comm Set.union_singleton coe_affineSpan_singleton direction_sup mem_affineSpan Set.mem_singleton direction_affineSpan vectorSpan_singleton sup_of_le_left
direction_affineSpan_pair_le_iff_exists_smul 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder direction affineSpan 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	—	direction_affineSpan vectorSpan_pair_rev Submodule.span_singleton_le_iff_mem Submodule.mem_span_singleton
direction_lt_of_nonempty 📖	mathematical	AffineSubspace Preorder.toLT PartialOrder.toPreorder instPartialOrder Set.Nonempty SetLike.coe instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder direction	—	lt_iff_le_and_exists SetLike.lt_iff_le_and_exists instIsConcreteLE direction_le vsub_mem_direction vsub_right_mem_direction_iff_mem
direction_sup 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	direction SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice Submodule.span Set Set.instSingletonSet VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	le_antisymm direction_affineSpan vectorSpan_eq_span_vsub_set_right Set.mem_union_left mem_coe Submodule.span_le sup_assoc sup_comm SetLike.mem_coe Submodule.mem_sup Submodule.zero_mem vsub_mem_direction zero_add vsub_add_vsub_cancel Submodule.mem_span_singleton_self sup_le sup_direction_le direction_eq_vectorSpan vectorSpan_def sInf_le_sInf Set.Subset.trans Set.singleton_subset_iff Set.vsub_mem_vsub mem_affineSpan Set.mem_union_right
direction_sup_eq_sup_direction 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	direction SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice	—	direction_sup vsub_self Submodule.span_zero_singleton sup_of_le_left
eq_univ_of_subsingleton_span_eq_top 📖	mathematical	Set.Subsingleton affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Set.univ	—	nonempty_of_affineSpan_eq_top Set.Subset.antisymm Set.subsingleton_iff_singleton Set.mem_univ Set.subsingleton_univ_iff subsingleton_of_subsingleton_span_eq_top
gc_map_comap 📖	mathematical	—	GaloisConnection AffineSubspace PartialOrder.toPreorder instPartialOrder map comap	—	map_le_iff_le_comap
inclusion_linear 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder	AffineMap.linear Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction instSetLike Submodule.addCommGroup Submodule.module toAddTorsor Nonempty.map Set.Elem SetLike.coe Set.inclusion inclusion Submodule.inclusion direction_le	—	Nonempty.map
inclusion_rfl 📖	mathematical	—	inclusion le_refl AffineSubspace PartialOrder.toPreorder instPartialOrder AffineMap.id Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction instSetLike Submodule.addCommGroup Submodule.module toAddTorsor	—	Nonempty.map le_refl
le_comap_map 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder comap map	—	GaloisConnection.le_u_l gc_map_comap
linear_topEquiv 📖	mathematical	—	AffineEquiv.linear AffineSubspace SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction Submodule.addCommGroup Submodule.module toAddTorsor instNonemptySubtypeMemTop topEquiv LinearEquiv.trans Submodule.instTop Submodule.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearEquiv.ofEq direction_top Submodule.topEquiv	—	instNonemptySubtypeMemTop
map_bot 📖	mathematical	—	map Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	coe_injective Set.image_empty
map_comap_le 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	GaloisConnection.l_u_le gc_map_comap
map_direction 📖	mathematical	—	direction map Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids AffineMap.linear	—	RingHomSurjective.ids AffineMap.map_vectorSpan
map_eq_bot_iff 📖	mathematical	—	map Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	coe_eq_bot_iff Set.image_eq_empty coe_map map_bot
map_iSup 📖	mathematical	—	map iSup AffineSubspace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_iSup gc_map_comap
map_id 📖	mathematical	—	map AffineMap.id	—	coe_injective Set.image_id
map_inf_eq 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	map AffineSubspace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	ext
map_inf_le 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder map SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	le_inf map_mono inf_le_left inf_le_right
map_le_iff_le_comap 📖	mathematical	—	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	Set.image_subset_iff
map_map 📖	mathematical	—	map AffineMap.comp	—	coe_injective Set.image_image
map_mk' 📖	mathematical	—	map mk' DFunLike.coe AffineMap AffineMap.instFunLike Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids AffineMap.linear	—	ext RingHomSurjective.ids AffineMap.linearMap_vsub vadd_vsub AffineMap.map_vadd vsub_vadd
map_mono 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder instPartialOrder	map	—	Set.image_mono
map_span 📖	mathematical	—	map affineSpan Set.image DFunLike.coe AffineMap AffineMap.instFunLike	—	Set.eq_empty_or_nonempty span_empty map_bot Set.image_empty ext_of_direction_eq RingHomSurjective.ids map_direction Submodule.map.congr_simp direction_affineSpan AffineMap.map_vectorSpan Set.mem_image_of_mem subset_affineSpan
map_sup 📖	mathematical	—	map AffineSubspace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_sup gc_map_comap
map_symm 📖	mathematical	—	map AffineEquiv.toAffineMap AffineEquiv.symm comap	—	coe_injective AffineEquiv.image_symm
mem_affineSpan_insert_iff 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	affineSpan Set Set.instInsert SetLike.coe 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	—	vsub_right_mem_direction_iff_mem mem_affineSpan Set.mem_insert_of_mem mem_coe direction_affineSpan_insert Submodule.mem_sup Submodule.mem_span_singleton vadd_mem_of_mem_direction vsub_eq_zero_iff_eq vsub_vadd_eq_vsub_sub sub_eq_zero vadd_vadd vsub_mem_direction vadd_vsub_assoc
mem_affineSpan_singleton 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike affineSpan Set Set.instSingletonSet	—	coe_affineSpan_singleton
mem_comap 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike comap DFunLike.coe AffineMap AffineMap.instFunLike	—	—
mem_map 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike map DFunLike.coe AffineMap AffineMap.instFunLike	—	—
mem_map_iff_mem_of_injective 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	AffineSubspace SetLike.instMembership instSetLike map	—	Function.Injective.mem_set_image
mem_map_of_mem 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	map DFunLike.coe AffineMap AffineMap.instFunLike	—	Set.mem_image_of_mem
parallel_bot_iff_eq_bot 📖	mathematical	—	Parallel Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	map_eq_bot_iff Parallel.refl
parallel_comm 📖	mathematical	—	Parallel	—	Parallel.symm
parallel_iff_direction_eq_and_eq_bot_iff_eq_bot 📖	mathematical	—	Parallel direction Bot.bot AffineSubspace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Parallel.direction_eq bot_parallel_iff_eq_bot parallel_bot_iff_eq_bot Iff.not nonempty_iff_ne_bot eq_iff_direction_eq_of_mem mem_map vsub_vadd RingHomSurjective.ids map_direction Submodule.map_id
preimage_coe_affineSpan_singleton 📖	mathematical	—	Set.preimage AffineSubspace SetLike.instMembership instSetLike affineSpan Set Set.instSingletonSet Set.univ	—	Set.eq_univ_of_forall mem_affineSpan_singleton
subsingleton_of_subsingleton_span_eq_top 📖	—	Set.Subsingleton affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—	nonempty_of_affineSpan_eq_top Set.Subset.antisymm Set.subsingleton_of_univ_subsingleton Set.subsingleton_iff_singleton Set.mem_univ top_coe coe_affineSpan_singleton ext_iff
subtype_apply 📖	mathematical	—	DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction AffineSubspace instSetLike Submodule.addCommGroup Submodule.module toAddTorsor AffineMap.instFunLike subtype	—	—
subtype_injective 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction Submodule.addCommGroup Submodule.module toAddTorsor AffineMap.instFunLike subtype	—	Subtype.coe_injective
subtype_linear 📖	mathematical	—	AffineMap.linear Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike direction AffineSubspace instSetLike Submodule.addCommGroup Submodule.module toAddTorsor subtype Submodule.subtype	—	—
topEquiv_apply 📖	mathematical	—	DFunLike.coe AffineEquiv AffineSubspace SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction Submodule.addCommGroup Submodule.module toAddTorsor instNonemptySubtypeMemTop EquivLike.toFunLike AffineEquiv.equivLike topEquiv Set Set.instMembership Set.univ	—	instNonemptySubtypeMemTop
topEquiv_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.univ DFunLike.coe AffineEquiv AffineSubspace SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction Submodule.addCommGroup Submodule.module toAddTorsor instNonemptySubtypeMemTop EquivLike.toFunLike AffineEquiv.equivLike AffineEquiv.symm topEquiv	—	instNonemptySubtypeMemTop
vectorSpan_union_of_mem_of_mem 📖	mathematical	Set Set.instMembership	vectorSpan Set.instUnion Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	span_union direction_sup_eq_sup_direction mem_affineSpan
vsub_left_mem_direction_iff_mem 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	mem_direction_iff_eq_vsub_left
vsub_right_mem_direction_iff_mem 📖	mathematical	AffineSubspace SetLike.instMembership instSetLike	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike direction VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	mem_direction_iff_eq_vsub_right

AffineSubspace.Parallel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
direction_eq 📖	mathematical	AffineSubspace.Parallel	AffineSubspace.direction	—	RingHomSurjective.ids AffineSubspace.map_direction Submodule.map_id
refl 📖	mathematical	—	AffineSubspace.Parallel	—	AffineEquiv.constVAdd_zero AffineSubspace.map_id
trans 📖	—	AffineSubspace.Parallel	—	—	AffineSubspace.map_map AffineEquiv.coe_trans_to_affineMap AffineEquiv.constVAdd_add
vectorSpan_eq 📖	mathematical	AffineSubspace.Parallel affineSpan	vectorSpan	—	direction_eq

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_coe_preimage_eq_top 📖	mathematical	—	affineSpan Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem Set.preimage Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem eq_top_iff affineSpan_induction' subset_affineSpan AffineSubspace.smul_vsub_vadd_mem
affineSpan_pair_eq_of_left_mem_of_ne 📖	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet	—	—	affineSpan_pair_eq_of_mem_of_mem_of_ne right_mem_affineSpan_pair
affineSpan_pair_eq_of_mem_of_mem_of_ne 📖	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet	—	—	le_antisymm affineSpan_pair_le_of_mem_of_mem vadd_left_mem_affineSpan_pair vsub_vadd sub_ne_zero sub_smul vsub_sub_vsub_cancel_right neg_mul neg_smul SemigroupAction.mul_smul eq_inv_smul_iff₀ neg_vsub_eq_vsub_rev smul_vsub_vadd_mem_affineSpan_pair one_smul
affineSpan_pair_eq_of_right_mem_of_ne 📖	—	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet	—	—	affineSpan_pair_eq_of_mem_of_mem_of_ne left_mem_affineSpan_pair
affineSpan_singleton_union_vadd_eq_top_of_span_eq_top 📖	mathematical	Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.range Set Set.instMembership Top.top Submodule Submodule.instTop	affineSpan Set.instUnion Set.instSingletonSet Set.image HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	AffineSubspace.ext_of_direction_eq direction_affineSpan AffineSubspace.direction_top vectorSpan_eq_span_vsub_set_right Set.mem_union_left Set.mem_singleton eq_top_iff Submodule.span_mono vadd_vsub mem_affineSpan AffineSubspace.mem_top
exists_eq_smul_of_parallel 📖	mathematical	AffineSubspace DivisionRing.toRing SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet AffineSubspace.Parallel Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder AffineSubspace.direction	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction	—	AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul' DivisionRing.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul Units.ne_zero DivisionRing.toNontrivial Units.smul_def neg_vsub_eq_vsub_rev smul_neg vsub_add_vsub_cancel smul_add add_comm neg_mem_iff AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass smul_vsub_mem_vectorSpan_pair smul_vsub_rev_mem_vectorSpan_pair sub_smul add_sub_add_left_eq_sub sub_mem AffineSubspace.vsub_left_mem_direction_iff_mem right_mem_affineSpan_pair direction_affineSpan Submodule.smul_mem_iff IsScalarTower.left sub_ne_zero
mem_affineSpan_pair_iff_exists_lineMap_eq 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap	—	vadd_left_mem_affineSpan_pair vsub_vadd AffineMap.lineMap_apply AffineMap.lineMap_mem_affineSpan_pair
mem_affineSpan_pair_iff_exists_lineMap_rev_eq 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineMap.lineMap	—	Set.pair_comm mem_affineSpan_pair_iff_exists_lineMap_eq
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	—	vectorSpan_pair Submodule.mem_span_singleton
mem_vectorSpan_pair_rev 📖	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	—	vectorSpan_pair_rev Submodule.mem_span_singleton
smul_vsub_rev_vadd_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet 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	—	AffineMap.lineMap_rev_mem_affineSpan_pair
smul_vsub_vadd_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet 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	—	AffineMap.lineMap_mem_affineSpan_pair
vadd_left_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet 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.vadd_mem_iff_mem_direction left_mem_affineSpan_pair direction_affineSpan mem_vectorSpan_pair_rev
vadd_right_mem_affineSpan_pair 📖	mathematical	—	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Set.instSingletonSet 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.vadd_mem_iff_mem_direction right_mem_affineSpan_pair direction_affineSpan mem_vectorSpan_pair
vectorSpan_eq_span_vsub_finset_right_ne 📖	mathematical	Finset Finset.instMembership	vectorSpan SetLike.coe Finset.instSetLike Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Finset.image VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Finset.erase	—	vectorSpan_eq_span_vsub_set_right_ne Finset.mem_coe Finset.coe_image Finset.coe_erase
vectorSpan_eq_span_vsub_set_left 📖	mathematical	Set Set.instMembership	vectorSpan Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.image VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vectorSpan_def le_antisymm Submodule.span_le vsub_sub_vsub_cancel_left SetLike.mem_coe Submodule.mem_span Submodule.sub_mem Submodule.span_mono
vectorSpan_eq_span_vsub_set_left_ne 📖	mathematical	Set Set.instMembership	vectorSpan Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.image VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Set.instSDiff Set.instSingletonSet	—	vectorSpan_eq_span_vsub_set_left Set.insert_eq_of_mem Set.insert_diff_singleton Set.image_insert_eq vsub_self Submodule.span_insert_eq_span AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
vectorSpan_eq_span_vsub_set_right 📖	mathematical	Set Set.instMembership	vectorSpan Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.image VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vectorSpan_def le_antisymm Submodule.span_le vsub_sub_vsub_cancel_right SetLike.mem_coe Submodule.mem_span Submodule.sub_mem Submodule.span_mono
vectorSpan_eq_span_vsub_set_right_ne 📖	mathematical	Set Set.instMembership	vectorSpan Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.image VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Set.instSDiff Set.instSingletonSet	—	vectorSpan_eq_span_vsub_set_right Set.insert_eq_of_mem Set.insert_diff_singleton Set.image_insert_eq vsub_self Submodule.span_insert_eq_span AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
vectorSpan_image_eq_span_vsub_set_left_ne 📖	mathematical	Set Set.instMembership	vectorSpan Set.image Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Set.instSDiff Set.instSingletonSet	—	vectorSpan_eq_span_vsub_set_left Set.mem_image_of_mem Set.insert_eq_of_mem Set.insert_diff_singleton Set.image_insert_eq vsub_self Submodule.span_insert_eq_span AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
vectorSpan_image_eq_span_vsub_set_right_ne 📖	mathematical	Set Set.instMembership	vectorSpan Set.image Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Set.instSDiff Set.instSingletonSet	—	vectorSpan_eq_span_vsub_set_right Set.mem_image_of_mem Set.insert_eq_of_mem Set.insert_diff_singleton Set.image_insert_eq vsub_self Submodule.span_insert_eq_span AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
vectorSpan_pair 📖	mathematical	—	vectorSpan Set Set.instInsert Set.instSingletonSet Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vectorSpan_eq_span_vsub_set_left Set.mem_insert Set.image_pair vsub_self Submodule.span_insert_zero
vectorSpan_pair_rev 📖	mathematical	—	vectorSpan Set Set.instInsert Set.instSingletonSet Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	Set.pair_comm vectorSpan_pair
vectorSpan_range_eq_span_range_vsub_left 📖	mathematical	—	vectorSpan Set.range Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vectorSpan_eq_span_vsub_set_left Set.mem_range_self Set.range_comp
vectorSpan_range_eq_span_range_vsub_left_ne 📖	mathematical	—	vectorSpan Set.range Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	Set.image_univ vectorSpan_image_eq_span_vsub_set_left_ne Set.mem_univ Set.ext
vectorSpan_range_eq_span_range_vsub_right 📖	mathematical	—	vectorSpan Set.range Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	vectorSpan_eq_span_vsub_set_right Set.mem_range_self Set.range_comp
vectorSpan_range_eq_span_range_vsub_right_ne 📖	mathematical	—	vectorSpan Set.range Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	Set.image_univ vectorSpan_image_eq_span_vsub_set_right_ne Set.mem_univ Set.ext
vectorSpan_vadd 📖	mathematical	—	vectorSpan HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction	—	Set.vadd_set_vsub_vadd_set

---

← Back to Index