Restrict

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Restrict.lean

Statistics

Metric	Count
Definitions restrict	1
Theorems bijective, coe_apply, injective, linear, linear_aux, surjective, nonempty_map	7
Total	8

AffineMap

Definitions

Name	Category	Theorems
restrict 📖	CompOp	6 math math: restrict.bijective, Affine.Simplex.restrict_map_restrict, restrict.injective, restrict.surjective, restrict.coe_apply, restrict.linear

AffineMap.restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike	Function.Bijective AffineSubspace SetLike.instMembership AffineSubspace.instSetLike AffineSubspace.map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor AffineSubspace.nonempty_map AffineMap.restrict le_refl PartialOrder.toPreorder AffineSubspace.instPartialOrder	—	AffineSubspace.nonempty_map le_refl injective surjective
coe_apply 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder AffineSubspace.map	SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor AffineMap.instFunLike AffineMap.restrict	—	—
injective 📖	mathematical	DFunLike.coe AffineMap AffineMap.instFunLike AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder AffineSubspace.map	SetLike.instMembership AffineSubspace.instSetLike Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor AffineMap.restrict	—	—
linear 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder AffineSubspace.map	AffineMap.linear Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AffineSubspace.direction AffineSubspace.instSetLike Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor AffineMap.restrict LinearMap.restrict linear_aux	—	—
linear_aux 📖	mathematical	AffineSubspace Preorder.toLE PartialOrder.toPreorder AffineSubspace.instPartialOrder AffineSubspace.map	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder AffineSubspace.direction Submodule.comap RingHom.id Semiring.toNonAssocSemiring AffineMap.linear	—	RingHomSurjective.ids Submodule.map_le_iff_le_comap AffineSubspace.map_direction AffineSubspace.direction_le
surjective 📖	mathematical	AffineSubspace.map	AffineSubspace SetLike.instMembership AffineSubspace.instSetLike DFunLike.coe AffineMap Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike AffineSubspace.direction Submodule.addCommGroup Submodule.module AffineSubspace.toAddTorsor AffineMap.instFunLike AffineMap.restrict le_of_eq PartialOrder.toPreorder AffineSubspace.instPartialOrder	—	le_of_eq AffineSubspace.mem_map

AffineSubspace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_map 📖	mathematical	—	AffineSubspace SetLike.instMembership instSetLike map	—	mem_map

---

← Back to Index