Side

📁 Source: Mathlib/Analysis/Convex/Side.lean

Statistics

Metric	Count
Definitions `SOppSide`, `SSameSide`, `WOppSide`, `WSameSide`	4
Theorems `sOppSide_affineSpan_faceOpposite_iff`, `sOppSide_affineSpan_faceOpposite_of_pos_of_neg`, `sOppSide_affineSpan_faceOpposite_point_left_iff`, `sOppSide_affineSpan_faceOpposite_point_right_iff`, `sSameSide_affineSpan_faceOpposite_iff`, `sSameSide_affineSpan_faceOpposite_of_sign_eq`, `sSameSide_affineSpan_faceOpposite_point_left_iff`, `sSameSide_affineSpan_faceOpposite_point_right_iff`, `wOppSide_affineSpan_faceOpposite_iff`, `wOppSide_affineSpan_faceOpposite_point_left_iff`, `wOppSide_affineSpan_faceOpposite_point_right_iff`, `wSameSide_affineSpan_faceOpposite_iff`, `wSameSide_affineSpan_faceOpposite_point_left_iff`, `wSameSide_affineSpan_faceOpposite_point_right_iff`, `sOppSide_map_iff`, `sSameSide_map_iff`, `wOppSide_map_iff`, `wSameSide_map_iff`, `exists_sbtw`, `left_notMem`, `nonempty`, `not_sSameSide`, `not_wSameSide`, `right_notMem`, `trans`, `trans_sSameSide`, `trans_wOppSide`, `trans_wSameSide`, `wOppSide`, `left_notMem`, `nonempty`, `not_sOppSide`, `not_wOppSide`, `right_notMem`, `trans`, `trans_sOppSide`, `trans_wOppSide`, `trans_wSameSide`, `wSameSide`, `map`, `nonempty`, `not_sSameSide`, `trans`, `trans_sOppSide`, `trans_sSameSide`, `trans_wSameSide`, `map`, `nonempty`, `not_sOppSide`, `trans`, `trans_sOppSide`, `trans_sSameSide`, `trans_wOppSide`, `isConnected_setOf_sOppSide`, `isConnected_setOf_sSameSide`, `isConnected_setOf_wOppSide`, `isConnected_setOf_wSameSide`, `isPreconnected_setOf_sOppSide`, `isPreconnected_setOf_sSameSide`, `isPreconnected_setOf_wOppSide`, `isPreconnected_setOf_wSameSide`, `not_sOppSide_bot`, `not_sOppSide_self`, `not_sSameSide_bot`, `not_wOppSide_bot`, `not_wSameSide_bot`, `sOppSide_comm`, `sOppSide_iff_exists_left`, `sOppSide_iff_exists_right`, `sOppSide_lineMap_left`, `sOppSide_lineMap_right`, `sOppSide_pointReflection`, `sOppSide_smul_vsub_vadd_left`, `sOppSide_smul_vsub_vadd_right`, `sOppSide_vadd_left_iff`, `sOppSide_vadd_right_iff`, `sSameSide_comm`, `sSameSide_iff_exists_left`, `sSameSide_iff_exists_right`, `sSameSide_lineMap_left`, `sSameSide_lineMap_right`, `sSameSide_self_iff`, `sSameSide_smul_vsub_vadd_left`, `sSameSide_smul_vsub_vadd_right`, `sSameSide_vadd_left_iff`, `sSameSide_vadd_right_iff`, `setOf_sOppSide_eq_image2`, `setOf_sSameSide_eq_image2`, `setOf_wOppSide_eq_image2`, `setOf_wSameSide_eq_image2`, `wOppSide_comm`, `wOppSide_iff_exists_left`, `wOppSide_iff_exists_right`, `wOppSide_iff_exists_wbtw`, `wOppSide_lineMap_left`, `wOppSide_lineMap_right`, `wOppSide_of_left_mem`, `wOppSide_of_right_mem`, `wOppSide_pointReflection`, `wOppSide_self_iff`, `wOppSide_smul_vsub_vadd_left`, `wOppSide_smul_vsub_vadd_right`, `wOppSide_vadd_left_iff`, `wOppSide_vadd_right_iff`, `wSameSide_and_wOppSide_iff`, `wSameSide_comm`, `wSameSide_iff_exists_left`, `wSameSide_iff_exists_right`, `wSameSide_lineMap_left`, `wSameSide_lineMap_right`, `wSameSide_of_left_mem`, `wSameSide_of_right_mem`, `wSameSide_self_iff`, `wSameSide_smul_vsub_vadd_left`, `wSameSide_smul_vsub_vadd_right`, `wSameSide_vadd_left_iff`, `wSameSide_vadd_right_iff`, `sOppSide_map_iff`, `sSameSide_map_iff`, `wOppSide_map_iff`, `wSameSide_map_iff`, `sOppSide_of_notMem_of_mem`, `wOppSide₁₃`, `wOppSide₃₁`, `wSameSide₁₂`, `wSameSide₂₁`, `wSameSide₂₃`, `wSameSide₃₂`	128
Total	132

Affine.Simplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sOppSide_affineSpan_faceOpposite_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.SOppSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `OrderHom` `SignType` `PartialOrder.toPreorder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearOrder.toDecidableLT` `SignType.instNeg`	—	`Iff.not` `affineCombination_mem_affineSpan_faceOpposite_iff` `AffineSubspace.SOppSide.left_notMem` `AffineSubspace.SOppSide.right_notMem` `sign_eq_sign_or_eq_neg` `AffineSubspace.WSameSide.not_sOppSide` `AffineSubspace.SSameSide.wSameSide` `sSameSide_affineSpan_faceOpposite_of_sign_eq` `Ne.lt_or_gt` `AffineSubspace.SOppSide.symm` `sOppSide_affineSpan_faceOpposite_of_pos_of_neg` `sign_eq_one_iff` `sign_neg` `sign_eq_neg_one_iff` `neg_eq_iff_eq_neg` `sign_pos`
`sOppSide_affineSpan_faceOpposite_of_pos_of_neg` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`AffineSubspace.SOppSide` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination`	—	`Finset.sum_congr` `Finset.sum_add_distrib` `Finset.sum_sub_distrib` `sub_self` `MulZeroClass.mul_zero` `zero_add` `sbtw_lineMap_iff` `IsStrictOrderedRing.toIsOrderedRing` `instIsDomain` `Pi.instModuleIsTorsionFree` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `div_lt_one` `Set.InjOn.sbtw_map_iff` `AffineIndependent.injOn_affineCombination_fintypeAffineCoords` `independent` `mem_fintypeAffineCoords_iff_sum` `Sbtw.sOppSide_of_notMem_of_mem` `Iff.not` `affineCombination_mem_affineSpan_faceOpposite_iff` `LT.lt.ne'` `neg_sub` `mul_neg` `div_mul_cancel₀` `neg_add_cancel`
`sOppSide_affineSpan_faceOpposite_point_left_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.SOppSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.affineCombination_affineCombinationSingleWeights` `Finset.mem_univ` `sOppSide_affineSpan_faceOpposite_iff` `Finset.sum_affineCombinationSingleWeights` `neg_eq_iff_eq_neg` `Finset.affineCombinationSingleWeights_apply_self` `sign_pos` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`sOppSide_affineSpan_faceOpposite_point_right_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.SOppSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`AffineSubspace.sOppSide_comm` `sOppSide_affineSpan_faceOpposite_point_left_iff`
`sSameSide_affineSpan_faceOpposite_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.SSameSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `OrderHom` `SignType` `PartialOrder.toPreorder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearOrder.toDecidableLT`	—	`Iff.not` `affineCombination_mem_affineSpan_faceOpposite_iff` `AffineSubspace.SSameSide.left_notMem` `AffineSubspace.SSameSide.right_notMem` `sign_eq_sign_or_eq_neg` `Ne.lt_or_gt` `AffineSubspace.WOppSide.not_sSameSide` `AffineSubspace.SOppSide.wOppSide` `AffineSubspace.SOppSide.symm` `sOppSide_affineSpan_faceOpposite_of_pos_of_neg` `sign_eq_one_iff` `sign_neg` `sign_eq_neg_one_iff` `neg_eq_iff_eq_neg` `sign_pos` `sSameSide_affineSpan_faceOpposite_of_sign_eq`
`sSameSide_affineSpan_faceOpposite_of_sign_eq` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearOrder.toDecidableLT`	`AffineSubspace.SSameSide` `affineSpan` `Set.range` `points` `faceOpposite` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination`	—	`sign_zero` `exists_ne` `Fin.instNontrivial` `Nat.instAtLeastTwoHAddOfNat` `range_faceOpposite_points` `EuclideanDomain.toNontrivial` `AffineSubspace.wSameSide_iff_exists_left` `Finset.affineCombination_affineCombinationSingleWeights` `Finset.mem_univ` `Finset.affineCombination_vsub` `Finset.sum_congr` `Finset.sum_sub_distrib` `Finset.sum_affineCombinationSingleWeights` `sub_self` `MulZeroClass.mul_zero` `sub_zero` `Finset.affineCombinationSingleWeights_apply_of_ne` `inv_mul_cancel₀` `mul_one` `affineCombination_mem_affineSpan_faceOpposite_iff` `SameRay.congr_simp` `smul_smul` `sub_sub_cancel` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `Ne.lt_or_gt` `LT.lt.le` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `sign_eq_neg_one_iff` `sign_neg` `inv_neg''` `IsOrderedRing.toPosMulMono` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `sign_eq_one_iff` `sign_pos` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Iff.not`
`sSameSide_affineSpan_faceOpposite_point_left_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.SSameSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.affineCombination_affineCombinationSingleWeights` `Finset.mem_univ` `sSameSide_affineSpan_faceOpposite_iff` `Finset.sum_affineCombinationSingleWeights` `Finset.affineCombinationSingleWeights_apply_self` `sign_pos` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`sSameSide_affineSpan_faceOpposite_point_right_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.SSameSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`AffineSubspace.sSameSide_comm` `sSameSide_affineSpan_faceOpposite_point_left_iff`
`wOppSide_affineSpan_faceOpposite_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.WOppSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `OrderHom` `SignType` `PartialOrder.toPreorder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearOrder.toDecidableLT` `SignType.instNeg`	—	`sign_zero` `neg_zero` `sOppSide_affineSpan_faceOpposite_iff` `Iff.not` `affineCombination_mem_affineSpan_faceOpposite_iff` `AffineSubspace.wOppSide_of_left_mem` `AffineSubspace.wOppSide_of_right_mem` `Ne.lt_or_gt` `AffineSubspace.SOppSide.wOppSide` `AffineSubspace.SOppSide.symm` `sOppSide_affineSpan_faceOpposite_of_pos_of_neg` `sign_eq_one_iff` `sign_neg` `sign_eq_neg_one_iff` `neg_eq_iff_eq_neg` `sign_pos`
`wOppSide_affineSpan_faceOpposite_point_left_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.WOppSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.affineCombination_affineCombinationSingleWeights` `Finset.mem_univ` `wOppSide_affineSpan_faceOpposite_iff` `Finset.sum_affineCombinationSingleWeights` `neg_eq_iff_eq_neg` `Finset.affineCombinationSingleWeights_apply_self` `sign_pos` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`wOppSide_affineSpan_faceOpposite_point_right_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.WOppSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`AffineSubspace.wOppSide_comm` `wOppSide_affineSpan_faceOpposite_point_left_iff`
`wSameSide_affineSpan_faceOpposite_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.WSameSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `OrderHom` `SignType` `PartialOrder.toPreorder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `LinearOrder.toDecidableLT`	—	`sign_zero` `sSameSide_affineSpan_faceOpposite_iff` `Iff.not` `affineCombination_mem_affineSpan_faceOpposite_iff` `AffineSubspace.wSameSide_of_left_mem` `AffineSubspace.wSameSide_of_right_mem` `AffineSubspace.SSameSide.wSameSide` `sSameSide_affineSpan_faceOpposite_of_sign_eq`
`wSameSide_affineSpan_faceOpposite_point_left_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.WSameSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.affineCombination_affineCombinationSingleWeights` `Finset.mem_univ` `wSameSide_affineSpan_faceOpposite_iff` `Finset.sum_affineCombinationSingleWeights` `Finset.affineCombinationSingleWeights_apply_self` `sign_pos` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`wSameSide_affineSpan_faceOpposite_point_right_iff` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Fin.fintype` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`AffineSubspace.WSameSide` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `affineSpan` `Set.range` `points` `faceOpposite` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`AffineSubspace.wSameSide_comm` `wSameSide_affineSpan_faceOpposite_point_left_iff`

AffineEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sOppSide_map_iff` 📖	mathematical	—	`AffineSubspace.SOppSide` `AffineSubspace.map` `CommRing.toRing` `toAffineMap` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`Function.Injective.sOppSide_map_iff` `injective`
`sSameSide_map_iff` 📖	mathematical	—	`AffineSubspace.SSameSide` `AffineSubspace.map` `CommRing.toRing` `toAffineMap` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`Function.Injective.sSameSide_map_iff` `injective`
`wOppSide_map_iff` 📖	mathematical	—	`AffineSubspace.WOppSide` `AffineSubspace.map` `CommRing.toRing` `toAffineMap` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`Function.Injective.wOppSide_map_iff` `injective`
`wSameSide_map_iff` 📖	mathematical	—	`AffineSubspace.WSameSide` `AffineSubspace.map` `CommRing.toRing` `toAffineMap` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`Function.Injective.wSameSide_map_iff` `injective`

AffineSubspace

Definitions

Name	Category	Theorems
`SOppSide` 📖	MathDef	32 math math: `sOppSide_iff_exists_right`, `AffineEquiv.sOppSide_map_iff`, `SSameSide.not_sOppSide`, `sOppSide_lineMap_left`, `sOppSide_vadd_right_iff`, `sOppSide_iff_exists_left`, `Affine.Simplex.ExcenterExists.sOppSide_excenter_point_iff`, `Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point`, `WSameSide.not_sOppSide`, `EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite`, `EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior`, `Affine.Simplex.sOppSide_excenter_singleton_point`, `Affine.Simplex.ExcenterExists.sOppSide_point_excenter_iff`, `sOppSide_lineMap_right`, `Function.Injective.sOppSide_map_iff`, `Affine.Simplex.sOppSide_point_excenter_singleton`, `Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg`, `sOppSide_pointReflection`, `not_sOppSide_bot`, `isPreconnected_setOf_sOppSide`, `Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton`, `isConnected_setOf_sOppSide`, `Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff`, `sOppSide_smul_vsub_vadd_left`, `setOf_sOppSide_eq_image2`, `not_sOppSide_self`, `Sbtw.sOppSide_of_notMem_of_mem`, `sOppSide_comm`, `Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff`, `sOppSide_vadd_left_iff`, `sOppSide_smul_vsub_vadd_right`, `Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff`
`SSameSide` 📖	MathDef	33 math math: `Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff`, `Affine.Simplex.sSameSide_excenter_singleton_point`, `sSameSide_vadd_right_iff`, `setOf_sSameSide_eq_image2`, `Affine.Triangle.sSameSide_affineSpan_pair_point_incenter`, `Affine.Simplex.sSameSide_incenter_point`, `sSameSide_iff_exists_left`, `sSameSide_self_iff`, `AffineEquiv.sSameSide_map_iff`, `not_sSameSide_bot`, `Function.Injective.sSameSide_map_iff`, `Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff`, `Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq`, `sSameSide_comm`, `sSameSide_lineMap_right`, `WOppSide.not_sSameSide`, `SOppSide.trans`, `SOppSide.not_sSameSide`, `sSameSide_smul_vsub_vadd_right`, `sSameSide_iff_exists_right`, `Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff`, `sSameSide_lineMap_left`, `sSameSide_vadd_left_iff`, `Affine.Simplex.sSameSide_point_excenter_singleton`, `Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton`, `Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point`, `sSameSide_smul_vsub_vadd_left`, `Affine.Triangle.sSameSide_affineSpan_pair_incenter_point`, `isConnected_setOf_sSameSide`, `Affine.Simplex.ExcenterExists.sSameSide_excenter_point_iff`, `Affine.Simplex.sSameSide_point_incenter`, `isPreconnected_setOf_sSameSide`, `Affine.Simplex.ExcenterExists.sSameSide_point_excenter_iff`
`WOppSide` 📖	MathDef	30 math math: `wOppSide_lineMap_right`, `Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff`, `wOppSide_smul_vsub_vadd_left`, `Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff`, `wOppSide_of_left_mem`, `Wbtw.wOppSide₁₃`, `wOppSide_comm`, `wOppSide_iff_exists_wbtw`, `isConnected_setOf_wOppSide`, `wOppSide_self_iff`, `SSameSide.not_wOppSide`, `wOppSide_iff_exists_left`, `setOf_wOppSide_eq_image2`, `SOppSide.wOppSide`, `wSameSide_and_wOppSide_iff`, `Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff`, `wOppSide_lineMap_left`, `isPreconnected_setOf_wOppSide`, `Wbtw.wOppSide₃₁`, `wOppSide_smul_vsub_vadd_right`, `SOppSide.trans_wSameSide`, `WSameSide.trans_sOppSide`, `AffineEquiv.wOppSide_map_iff`, `wOppSide_of_right_mem`, `wOppSide_iff_exists_right`, `wOppSide_vadd_right_iff`, `not_wOppSide_bot`, `wOppSide_pointReflection`, `wOppSide_vadd_left_iff`, `Function.Injective.wOppSide_map_iff`
`WSameSide` 📖	MathDef	31 math math: `Wbtw.wSameSide₂₁`, `Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff`, `not_wSameSide_bot`, `Wbtw.wSameSide₂₃`, `SOppSide.not_wSameSide`, `wSameSide_comm`, `WOppSide.trans_sOppSide`, `Wbtw.wSameSide₁₂`, `Wbtw.wSameSide₃₂`, `Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff`, `wSameSide_and_wOppSide_iff`, `SSameSide.wSameSide`, `wSameSide_vadd_left_iff`, `Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff`, `isConnected_setOf_wSameSide`, `wSameSide_lineMap_left`, `AffineEquiv.wSameSide_map_iff`, `WOppSide.trans`, `wSameSide_iff_exists_left`, `wSameSide_smul_vsub_vadd_left`, `wSameSide_self_iff`, `isPreconnected_setOf_wSameSide`, `wSameSide_of_left_mem`, `wSameSide_iff_exists_right`, `wSameSide_of_right_mem`, `wSameSide_smul_vsub_vadd_right`, `wSameSide_vadd_right_iff`, `wSameSide_lineMap_right`, `SOppSide.trans_wOppSide`, `Function.Injective.wSameSide_map_iff`, `setOf_wSameSide_eq_image2`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConnected_setOf_sOppSide` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `SetLike.instMembership` `instSetLike` `Set.Nonempty` `SetLike.coe`	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `SOppSide` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing`	—	`Real.instIsStrictOrderedRing` `setOf_sOppSide_eq_image2` `Set.image_prod` `IsConnected.image` `IsConnected.prod` `isConnected_Iio` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `isConnected_iff_connectedSpace` `AddTorsor.connectedSpace` `ConnectedSpace.toPreconnectedSpace` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace` `IsScalarTower.left` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor_1` `Continuous.continuousOn` `Continuous.vadd` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_fst` `continuous_const` `continuous_snd`
`isConnected_setOf_sSameSide` 📖	mathematical	`AffineSubspace` `Real` `Real.instRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `SetLike.instMembership` `instSetLike` `Set.Nonempty` `SetLike.coe`	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `SSameSide` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing`	—	`Real.instIsStrictOrderedRing` `setOf_sSameSide_eq_image2` `Set.image_prod` `IsConnected.image` `IsConnected.prod` `isConnected_Ioi` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `isConnected_iff_connectedSpace` `AddTorsor.connectedSpace` `ConnectedSpace.toPreconnectedSpace` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace` `IsScalarTower.left` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor_1` `Continuous.continuousOn` `Continuous.vadd` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_fst` `continuous_const` `continuous_snd`
`isConnected_setOf_wOppSide` 📖	mathematical	`Set.Nonempty` `SetLike.coe` `AffineSubspace` `Real` `Real.instRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `instSetLike`	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `WOppSide` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing`	—	`Real.instIsStrictOrderedRing` `AddTorsor.connectedSpace` `ConnectedSpace.toPreconnectedSpace` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor_1` `isConnected_univ` `setOf_wOppSide_eq_image2` `Set.image_prod` `IsConnected.image` `IsConnected.prod` `isConnected_Iic` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `isConnected_iff_connectedSpace` `IsScalarTower.left` `Continuous.continuousOn` `Continuous.vadd` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_fst` `continuous_const` `continuous_snd`
`isConnected_setOf_wSameSide` 📖	mathematical	`Set.Nonempty` `SetLike.coe` `AffineSubspace` `Real` `Real.instRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `instSetLike`	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `WSameSide` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing`	—	`Real.instIsStrictOrderedRing` `AddTorsor.connectedSpace` `ConnectedSpace.toPreconnectedSpace` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor_1` `isConnected_univ` `setOf_wSameSide_eq_image2` `Set.image_prod` `IsConnected.image` `IsConnected.prod` `isConnected_Ici` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `isConnected_iff_connectedSpace` `IsScalarTower.left` `Continuous.continuousOn` `Continuous.vadd` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_fst` `continuous_const` `continuous_snd`
`isPreconnected_setOf_sOppSide` 📖	mathematical	—	`IsPreconnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `SOppSide` `Real` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor`	—	`Real.instIsStrictOrderedRing` `Set.eq_empty_or_nonempty` `SOppSide.congr_simp` `coe_eq_bot_iff` `isPreconnected_empty` `IsConnected.isPreconnected` `isConnected_setOf_sOppSide`
`isPreconnected_setOf_sSameSide` 📖	mathematical	—	`IsPreconnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `SSameSide` `Real` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor`	—	`Real.instIsStrictOrderedRing` `Set.eq_empty_or_nonempty` `SSameSide.congr_simp` `coe_eq_bot_iff` `isPreconnected_empty` `IsConnected.isPreconnected` `isConnected_setOf_sSameSide`
`isPreconnected_setOf_wOppSide` 📖	mathematical	—	`IsPreconnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `WOppSide` `Real` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor`	—	`Real.instIsStrictOrderedRing` `Set.eq_empty_or_nonempty` `WOppSide.congr_simp` `coe_eq_bot_iff` `isPreconnected_empty` `IsConnected.isPreconnected` `isConnected_setOf_wOppSide`
`isPreconnected_setOf_wSameSide` 📖	mathematical	—	`IsPreconnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `WSameSide` `Real` `Real.commRing` `Real.partialOrder` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor`	—	`Real.instIsStrictOrderedRing` `Set.eq_empty_or_nonempty` `WSameSide.congr_simp` `coe_eq_bot_iff` `isPreconnected_empty` `IsConnected.isPreconnected` `isConnected_setOf_wSameSide`
`not_sOppSide_bot` 📖	mathematical	—	`SOppSide` `Bot.bot` `AffineSubspace` `CommRing.toRing` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`not_wOppSide_bot` `SOppSide.wOppSide`
`not_sOppSide_self` 📖	mathematical	—	`SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`SOppSide.eq_1`
`not_sSameSide_bot` 📖	mathematical	—	`SSameSide` `Bot.bot` `AffineSubspace` `CommRing.toRing` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`not_wSameSide_bot` `SSameSide.wSameSide`
`not_wOppSide_bot` 📖	mathematical	—	`WOppSide` `Bot.bot` `AffineSubspace` `CommRing.toRing` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`not_wSameSide_bot` 📖	mathematical	—	`WSameSide` `Bot.bot` `AffineSubspace` `CommRing.toRing` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`sOppSide_comm` 📖	mathematical	—	`SOppSide`	—	`SOppSide.eq_1` `wOppSide_comm`
`sOppSide_iff_exists_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`SOppSide.eq_1` `wOppSide_iff_exists_left`
`sOppSide_iff_exists_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`SOppSide.eq_1` `wOppSide_iff_exists_right`
`sOppSide_lineMap_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SOppSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`sOppSide_smul_vsub_vadd_left`
`sOppSide_lineMap_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SOppSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`SOppSide.symm` `sOppSide_lineMap_left`
`sOppSide_pointReflection` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.pointReflection`	—	`Sbtw.sOppSide_of_notMem_of_mem` `sbtw_pointReflection_of_ne`
`sOppSide_smul_vsub_vadd_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SOppSide` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`wOppSide_smul_vsub_vadd_left` `LT.lt.le` `vsub_right_mem_direction_iff_mem` `Submodule.smul_mem_iff` `IsScalarTower.left` `LT.lt.ne` `vadd_mem_iff_mem_direction`
`sOppSide_smul_vsub_vadd_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SOppSide` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`SOppSide.symm` `sOppSide_smul_vsub_vadd_left`
`sOppSide_vadd_left_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`SOppSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`SOppSide.eq_1` `wOppSide_vadd_left_iff` `vadd_mem_iff_mem_of_mem_direction`
`sOppSide_vadd_right_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`SOppSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`sOppSide_comm` `sOppSide_vadd_left_iff`
`sSameSide_comm` 📖	mathematical	—	`SSameSide`	—	`SSameSide.eq_1` `wSameSide_comm`
`sSameSide_iff_exists_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`SSameSide.eq_1` `wSameSide_iff_exists_left`
`sSameSide_iff_exists_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`sSameSide_comm` `sSameSide_iff_exists_left`
`sSameSide_lineMap_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SSameSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`sSameSide_smul_vsub_vadd_left`
`sSameSide_lineMap_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SSameSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`SSameSide.symm` `sSameSide_lineMap_left`
`sSameSide_self_iff` 📖	mathematical	—	`SSameSide` `Set.Nonempty` `SetLike.coe` `AffineSubspace` `CommRing.toRing` `instSetLike` `SetLike.instMembership`	—	`wSameSide_self_iff`
`sSameSide_smul_vsub_vadd_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SSameSide` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`wSameSide_smul_vsub_vadd_left` `LT.lt.le` `vsub_right_mem_direction_iff_mem` `Submodule.smul_mem_iff` `IsScalarTower.left` `LT.lt.ne` `vadd_mem_iff_mem_direction`
`sSameSide_smul_vsub_vadd_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`SSameSide` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`SSameSide.symm` `sSameSide_smul_vsub_vadd_left`
`sSameSide_vadd_left_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`SSameSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`SSameSide.eq_1` `wSameSide_vadd_left_iff` `vadd_mem_iff_mem_of_mem_direction`
`sSameSide_vadd_right_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`SSameSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`sSameSide_comm` `sSameSide_vadd_left_iff`
`setOf_sOppSide_eq_image2` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`setOf` `SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image2` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `Set.Iio` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe`	—	`Set.ext` `sOppSide_iff_exists_left` `vsub_eq_zero_iff_eq` `div_neg_of_neg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Left.neg_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `div_eq_inv_mul` `smul_smul` `neg_smul` `smul_neg` `inv_mul_cancel₀` `LT.lt.ne` `one_smul` `neg_vsub_eq_vsub_rev` `vsub_vadd` `sOppSide_smul_vsub_vadd_right`
`setOf_sSameSide_eq_image2` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`setOf` `SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image2` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `Set.Ioi` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe`	—	`Set.ext` `sSameSide_iff_exists_left` `vsub_eq_zero_iff_eq` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `div_eq_inv_mul` `smul_smul` `inv_mul_cancel₀` `LT.lt.ne` `one_smul` `vsub_vadd` `sSameSide_smul_vsub_vadd_right`
`setOf_wOppSide_eq_image2` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`setOf` `WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image2` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `Set.Iic` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe`	—	`Set.ext` `wOppSide_iff_exists_left` `vsub_eq_zero_iff_eq` `le_rfl` `zero_smul` `zero_vadd` `LT.lt.le` `div_neg_of_neg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Left.neg_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `div_eq_inv_mul` `smul_smul` `neg_smul` `smul_neg` `inv_mul_cancel₀` `LT.lt.ne` `one_smul` `neg_vsub_eq_vsub_rev` `vsub_vadd` `wOppSide_smul_vsub_vadd_right`
`setOf_wSameSide_eq_image2` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`setOf` `WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image2` `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` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `Set.Ici` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.coe`	—	`Set.ext` `wSameSide_iff_exists_left` `vsub_eq_zero_iff_eq` `le_rfl` `zero_smul` `zero_vadd` `LT.lt.le` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `div_eq_inv_mul` `smul_smul` `inv_mul_cancel₀` `LT.lt.ne` `one_smul` `vsub_vadd` `wSameSide_smul_vsub_vadd_right`
`wOppSide_comm` 📖	mathematical	—	`WOppSide`	—	`SameRay.sameRay_comm` `sameRay_neg_iff` `neg_vsub_eq_vsub_rev`
`wOppSide_iff_exists_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`vsub_eq_zero_iff_eq` `SameRay.zero_right` `smul_vsub_vadd_mem` `vadd_vsub_assoc` `vsub_sub_vsub_cancel_right` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `add_zero` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `eq_intCast` `Int.cast_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Int.cast_neg` `mul_neg` `neg_div` `neg_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `wOppSide_of_left_mem`
`wOppSide_iff_exists_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`wOppSide_comm` `wOppSide_iff_exists_left` `SameRay.sameRay_comm` `sameRay_neg_iff` `neg_vsub_eq_vsub_rev`
`wOppSide_iff_exists_wbtw` 📖	mathematical	—	`WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Wbtw`	—	`vsub_eq_zero_iff_eq` `wbtw_self_left` `IsStrictOrderedRing.toIsOrderedRing` `wbtw_self_right` `neg_vsub_eq_vsub_rev` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.smul_const_eq` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.neg_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `add_zero` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `eq_intCast` `Int.cast_neg` `Int.cast_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `mul_neg` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `add_pos'` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `AffineMap.lineMap_apply` `vsub_vadd` `vsub_vadd_eq_vsub_sub` `vadd_vsub_assoc` `vadd_assoc` `VAddAssocClass.left` `vadd_eq_add` `smul_vsub_vadd_mem` `Set.mem_image_of_mem` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `LT.lt.le` `Left.add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Wbtw.wOppSide₁₃`
`wOppSide_lineMap_left` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WOppSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`wOppSide_smul_vsub_vadd_left`
`wOppSide_lineMap_right` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WOppSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`WOppSide.symm` `wOppSide_lineMap_left`
`wOppSide_of_left_mem` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike`	`WOppSide`	—	`vsub_self` `SameRay.zero_left`
`wOppSide_of_right_mem` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike`	`WOppSide`	—	`WOppSide.symm` `wOppSide_of_left_mem`
`wOppSide_pointReflection` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.pointReflection`	—	`Wbtw.wOppSide₁₃` `wbtw_pointReflection`
`wOppSide_self_iff` 📖	mathematical	—	`WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	—	`SameRay.exists_eq_smul_add` `eq_vadd_iff_vsub_eq` `vsub_add_vsub_cancel` `add_comm` `smul_vsub_vadd_mem` `SameRay.rfl`
`wOppSide_smul_vsub_vadd_left` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WOppSide` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`vadd_vsub` `neg_neg` `neg_smul` `smul_neg` `neg_vsub_eq_vsub_rev` `SameRay.sameRay_nonneg_smul_left` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left` `neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono`
`wOppSide_smul_vsub_vadd_right` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WOppSide` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`WOppSide.symm` `wOppSide_smul_vsub_vadd_left`
`wOppSide_vadd_left_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`WOppSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`vadd_mem_of_mem_direction` `Submodule.neg_mem` `vsub_vadd_eq_vsub_sub` `sub_neg_eq_add` `add_comm` `vadd_vsub_assoc` `vadd_vsub_vadd_cancel_left`
`wOppSide_vadd_right_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`WOppSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`wOppSide_comm` `wOppSide_vadd_left_iff`
`wSameSide_and_wOppSide_iff` 📖	mathematical	—	`WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WOppSide` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	—	`wOppSide_self_iff` `WSameSide.trans_wOppSide` `wOppSide_comm` `wSameSide_of_left_mem` `wOppSide_of_left_mem` `wSameSide_of_right_mem` `wOppSide_of_right_mem`
`wSameSide_comm` 📖	mathematical	—	`WSameSide`	—	`SameRay.symm`
`wSameSide_iff_exists_left` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`vsub_eq_zero_iff_eq` `SameRay.zero_right` `smul_vsub_vadd_mem` `vsub_vadd_eq_vsub_sub` `smul_sub` `smul_smul` `mul_div_cancel₀` `LT.lt.ne` `vsub_sub_vsub_cancel_right` `wSameSide_of_left_mem`
`wSameSide_iff_exists_right` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup`	—	`wSameSide_comm` `wSameSide_iff_exists_left`
`wSameSide_lineMap_left` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WSameSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`wSameSide_smul_vsub_vadd_left`
`wSameSide_lineMap_right` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WSameSide` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`WSameSide.symm` `wSameSide_lineMap_left`
`wSameSide_of_left_mem` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike`	`WSameSide`	—	`vsub_self` `SameRay.zero_left`
`wSameSide_of_right_mem` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike`	`WSameSide`	—	`WSameSide.symm` `wSameSide_of_left_mem`
`wSameSide_self_iff` 📖	mathematical	—	`WSameSide` `Set.Nonempty` `SetLike.coe` `AffineSubspace` `CommRing.toRing` `instSetLike`	—	`WSameSide.nonempty` `SameRay.rfl`
`wSameSide_smul_vsub_vadd_left` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WSameSide` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`vadd_vsub` `SameRay.sameRay_nonneg_smul_left` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left`
`wSameSide_smul_vsub_vadd_right` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WSameSide` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `VSub.vsub` `AddTorsor.toVSub`	—	`WSameSide.symm` `wSameSide_smul_vsub_vadd_left`
`wSameSide_vadd_left_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`WSameSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`vadd_mem_of_mem_direction` `Submodule.neg_mem` `vsub_vadd_eq_vsub_sub` `sub_neg_eq_add` `add_comm` `vadd_vsub_assoc` `vadd_vsub_vadd_cancel_left`
`wSameSide_vadd_right_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction`	`WSameSide` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`wSameSide_comm` `wSameSide_vadd_left_iff`

AffineSubspace.SOppSide

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sbtw` 📖	mathematical	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `Sbtw`	—	`AffineSubspace.wOppSide_iff_exists_wbtw` `wOppSide`
`left_notMem` 📖	mathematical	`AffineSubspace.SOppSide`	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	—	—
`nonempty` 📖	mathematical	`AffineSubspace.SOppSide`	`Set.Nonempty` `SetLike.coe` `AffineSubspace` `CommRing.toRing` `AffineSubspace.instSetLike`	—	—
`not_sSameSide` 📖	mathematical	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace.SSameSide`	—	`not_wSameSide`
`not_wSameSide` 📖	mathematical	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace.WSameSide`	—	`AffineSubspace.WSameSide.not_sOppSide`
`right_notMem` 📖	mathematical	`AffineSubspace.SOppSide`	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	—	—
`trans` 📖	mathematical	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace.SSameSide`	—	`trans_wOppSide`
`trans_sSameSide` 📖	—	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.SSameSide`	—	—	`symm` `AffineSubspace.SSameSide.trans_sOppSide` `AffineSubspace.SSameSide.symm`
`trans_wOppSide` 📖	mathematical	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.WOppSide`	`AffineSubspace.WSameSide`	—	`AffineSubspace.WSameSide.symm` `AffineSubspace.WOppSide.trans_sOppSide` `AffineSubspace.WOppSide.symm` `symm`
`trans_wSameSide` 📖	mathematical	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.WSameSide`	`AffineSubspace.WOppSide`	—	`AffineSubspace.WOppSide.symm` `AffineSubspace.WSameSide.trans_sOppSide` `AffineSubspace.WSameSide.symm` `symm`
`wOppSide` 📖	mathematical	`AffineSubspace.SOppSide`	`AffineSubspace.WOppSide`	—	—

AffineSubspace.SSameSide

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_notMem` 📖	mathematical	`AffineSubspace.SSameSide`	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	—	—
`nonempty` 📖	mathematical	`AffineSubspace.SSameSide`	`Set.Nonempty` `SetLike.coe` `AffineSubspace` `CommRing.toRing` `AffineSubspace.instSetLike`	—	—
`not_sOppSide` 📖	mathematical	`AffineSubspace.SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace.SOppSide`	—	`not_wOppSide`
`not_wOppSide` 📖	mathematical	`AffineSubspace.SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace.WOppSide`	—	`AffineSubspace.wSameSide_and_wOppSide_iff`
`right_notMem` 📖	mathematical	`AffineSubspace.SSameSide`	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	—	—
`trans` 📖	—	`AffineSubspace.SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`AffineSubspace.WSameSide.trans_sSameSide` `wSameSide`
`trans_sOppSide` 📖	—	`AffineSubspace.SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.SOppSide`	—	—	`trans_wOppSide`
`trans_wOppSide` 📖	—	`AffineSubspace.SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.WOppSide`	—	—	`AffineSubspace.WSameSide.trans_wOppSide` `wSameSide`
`trans_wSameSide` 📖	—	`AffineSubspace.SSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.WSameSide`	—	—	`AffineSubspace.WSameSide.symm` `AffineSubspace.WSameSide.trans_sSameSide` `symm`
`wSameSide` 📖	mathematical	`AffineSubspace.SSameSide`	`AffineSubspace.WSameSide`	—	—

AffineSubspace.WOppSide

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`AffineSubspace.WOppSide`	`AffineSubspace.map` `CommRing.toRing` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	—	`AffineSubspace.mem_map_of_mem` `SameRay.congr_simp` `SameRay.map`
`nonempty` 📖	mathematical	`AffineSubspace.WOppSide`	`Set.Nonempty` `SetLike.coe` `AffineSubspace` `CommRing.toRing` `AffineSubspace.instSetLike`	—	—
`not_sSameSide` 📖	mathematical	`AffineSubspace.WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace.SSameSide`	—	`AffineSubspace.SSameSide.not_wOppSide`
`trans` 📖	mathematical	`AffineSubspace.WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.WSameSide`	—	`AffineSubspace.wOppSide_iff_exists_left` `SameRay.trans` `neg_vsub_eq_vsub_rev` `sameRay_neg_iff` `vsub_eq_zero_iff_eq`
`trans_sOppSide` 📖	mathematical	`AffineSubspace.WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.SOppSide`	`AffineSubspace.WSameSide`	—	`trans`
`trans_sSameSide` 📖	—	`AffineSubspace.WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.SSameSide`	—	—	`trans_wSameSide`
`trans_wSameSide` 📖	—	`AffineSubspace.WOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.WSameSide` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	—	—	`symm` `AffineSubspace.WSameSide.trans_wOppSide` `AffineSubspace.WSameSide.symm`

AffineSubspace.WSameSide

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`AffineSubspace.WSameSide`	`AffineSubspace.map` `CommRing.toRing` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	—	`AffineSubspace.mem_map_of_mem` `SameRay.congr_simp` `SameRay.map`
`nonempty` 📖	mathematical	`AffineSubspace.WSameSide`	`Set.Nonempty` `SetLike.coe` `AffineSubspace` `CommRing.toRing` `AffineSubspace.instSetLike`	—	—
`not_sOppSide` 📖	mathematical	`AffineSubspace.WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AffineSubspace.SOppSide`	—	`AffineSubspace.wSameSide_and_wOppSide_iff`
`trans` 📖	—	`AffineSubspace.WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	—	—	`AffineSubspace.wSameSide_iff_exists_left` `SameRay.trans` `vsub_eq_zero_iff_eq`
`trans_sOppSide` 📖	mathematical	`AffineSubspace.WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.SOppSide`	`AffineSubspace.WOppSide`	—	`trans_wOppSide`
`trans_sSameSide` 📖	—	`AffineSubspace.WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.SSameSide`	—	—	`trans`
`trans_wOppSide` 📖	—	`AffineSubspace.WSameSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace.WOppSide` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	—	—	`AffineSubspace.wOppSide_iff_exists_left` `SameRay.trans` `vsub_eq_zero_iff_eq`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sOppSide_map_iff` 📖	mathematical	`DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike`	`AffineSubspace.SOppSide` `AffineSubspace.map`	—	`wOppSide_map_iff` `AffineSubspace.mem_map_iff_mem_of_injective`
`sSameSide_map_iff` 📖	mathematical	`DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike`	`AffineSubspace.SSameSide` `AffineSubspace.map`	—	`wSameSide_map_iff` `AffineSubspace.mem_map_iff_mem_of_injective`
`wOppSide_map_iff` 📖	mathematical	`DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike`	`AffineSubspace.WOppSide` `AffineSubspace.map`	—	`AffineSubspace.mem_map` `sameRay_map_iff` `LinearMap.semilinearMapClass` `AffineMap.linear_injective_iff` `SameRay.congr_simp` `AffineSubspace.WOppSide.map`
`wSameSide_map_iff` 📖	mathematical	`DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike`	`AffineSubspace.WSameSide` `AffineSubspace.map`	—	`AffineSubspace.mem_map` `sameRay_map_iff` `LinearMap.semilinearMapClass` `AffineMap.linear_injective_iff` `SameRay.congr_simp` `AffineSubspace.WSameSide.map`

Sbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sOppSide_of_notMem_of_mem` 📖	mathematical	`Sbtw` `DivisionRing.toRing` `Field.toDivisionRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.SOppSide` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Wbtw.wOppSide₁₃` `wbtw` `one_smul` `vsub_vadd` `AffineMap.lineMap_apply` `AffineSubspace.vsub_mem_direction` `AffineSubspace.vadd_mem_iff_mem_of_mem_direction` `Submodule.smul_mem` `Submodule.smul_mem_iff` `IsScalarTower.left` `sub_ne_zero_of_ne` `sub_eq_add_neg` `add_smul` `neg_one_smul` `neg_vsub_eq_vsub_rev` `vadd_vsub_assoc`

Wbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wOppSide₁₃` 📖	mathematical	`Wbtw` `CommRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.WOppSide`	—	`LE.le.lt_or_eq` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `AffineMap.lineMap_apply` `vadd_vsub_assoc` `vsub_vadd_eq_vsub_sub` `neg_vsub_eq_vsub_rev` `vsub_self` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.neg_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `eq_intCast` `Int.cast_neg` `Int.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `SameRay.congr_simp` `AffineMap.lineMap_apply_zero` `AffineMap.lineMap_apply_one`
`wOppSide₃₁` 📖	mathematical	`Wbtw` `CommRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.WOppSide`	—	`wOppSide₁₃` `symm` `IsStrictOrderedRing.toIsOrderedRing`
`wSameSide₁₂` 📖	mathematical	`Wbtw` `CommRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.WSameSide`	—	`wSameSide₃₂` `symm` `IsStrictOrderedRing.toIsOrderedRing`
`wSameSide₂₁` 📖	mathematical	`Wbtw` `CommRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.WSameSide`	—	`wSameSide₂₃` `symm` `IsStrictOrderedRing.toIsOrderedRing`
`wSameSide₂₃` 📖	mathematical	`Wbtw` `CommRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.WSameSide`	—	`AffineSubspace.wSameSide_lineMap_left`
`wSameSide₃₂` 📖	mathematical	`Wbtw` `CommRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineSubspace.WSameSide`	—	`AffineSubspace.WSameSide.symm` `wSameSide₂₃`

---

← Back to Index