Subspace

📁 Source: Mathlib/LinearAlgebra/Projectivization/Subspace.lean

Statistics

Metric	Count
Definitions `Subspace`, `Subspace`, `carrier`, `gi`, `instCompleteLattice`, `instInf`, `instInfSet`, `instPartialOrder`, `instSetLike`, `span`, `spanCarrier`, `submodule`, `subspaceInhabited`, `projectivization`, `Subspace`	15
Theorems `ext`, `ext_iff`, `mem_add`, `mem_add'`, `mem_carrier_iff`, `mem_span`, `mem_submodule_iff`, `monotone_span`, `span_coe`, `span_empty`, `span_eq_of_le`, `span_eq_sInf`, `span_eq_span_iff`, `span_iUnion`, `span_le_span`, `span_le_subspace_iff`, `span_sup`, `span_union`, `span_univ`, `subset_span`, `subset_span_trans`, `sup_span`, `mem_projectivization_iff_submodule_le`, `mk_mem_projectivization_iff`	24
Total	39

Combinatorics

Definitions

Name	Category	Theorems
`Subspace` 📖	CompData	1 math math: `Subspace.coe_injective`

Projectivization

Definitions

Name	Category	Theorems
`Subspace` 📖	CompData	18 math math: `Subspace.span_sup`, `Subspace.span_le_span`, `Subspace.span_empty`, `Subspace.span_coe`, `Submodule.mk_mem_projectivization_iff`, `Subspace.subset_span`, `Submodule.mem_projectivization_iff_submodule_le`, `Subspace.sup_span`, `Subspace.monotone_span`, `Subspace.span_le_subspace_iff`, `Subspace.mem_span`, `Subspace.span_union`, `Subspace.span_univ`, `Subspace.span_eq_span_iff`, `Subspace.mem_carrier_iff`, `Subspace.span_eq_sInf`, `Subspace.span_iUnion`, `Subspace.mem_submodule_iff`

Projectivization.Subspace

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	2 math math: `ext_iff`, `mem_carrier_iff`
`gi` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	6 math math: `span_sup`, `span_empty`, `sup_span`, `span_union`, `span_univ`, `span_iUnion`
`instInf` 📖	CompOp	—
`instInfSet` 📖	CompOp	1 math math: `span_eq_sInf`
`instPartialOrder` 📖	CompOp	6 math math: `span_le_span`, `Submodule.mk_mem_projectivization_iff`, `Submodule.mem_projectivization_iff_submodule_le`, `monotone_span`, `span_le_subspace_iff`, `mem_submodule_iff`
`instSetLike` 📖	CompOp	12 math math: `span_sup`, `span_coe`, `Submodule.mk_mem_projectivization_iff`, `subset_span`, `Submodule.mem_projectivization_iff_submodule_le`, `sup_span`, `span_le_subspace_iff`, `mem_span`, `span_eq_span_iff`, `mem_carrier_iff`, `span_eq_sInf`, `mem_submodule_iff`
`span` 📖	CompOp	14 math math: `span_sup`, `span_le_span`, `span_empty`, `span_coe`, `subset_span`, `sup_span`, `monotone_span`, `span_le_subspace_iff`, `mem_span`, `span_union`, `span_univ`, `span_eq_span_iff`, `span_eq_sInf`, `span_iUnion`
`spanCarrier` 📖	CompData	—
`submodule` 📖	CompOp	1 math math: `mem_submodule_iff`
`subspaceInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`carrier`	—	—	—
`ext_iff` 📖	mathematical	—	`carrier`	—	`ext`
`mem_add` 📖	mathematical	`Projectivization` `Field.toDivisionRing` `Projectivization.Subspace` `SetLike.instMembership` `instSetLike`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`mem_add'`
`mem_add'` 📖	mathematical	`Projectivization` `Field.toDivisionRing` `Set` `Set.instMembership` `carrier`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`mem_carrier_iff` 📖	mathematical	—	`Projectivization` `Field.toDivisionRing` `Set` `Set.instMembership` `carrier` `Projectivization.Subspace` `SetLike.instMembership` `instSetLike`	—	—
`mem_span` 📖	mathematical	—	`Projectivization` `Field.toDivisionRing` `Projectivization.Subspace` `SetLike.instMembership` `instSetLike` `span`	—	`le_refl`
`mem_submodule_iff` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `OrderIso` `Projectivization.Subspace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderIso` `submodule` `Projectivization` `Field.toDivisionRing` `instSetLike`	—	—
`monotone_span` 📖	mathematical	—	`Monotone` `Set` `Projectivization` `Field.toDivisionRing` `Projectivization.Subspace` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrder` `span`	—	`GaloisConnection.monotone_l` `GaloisInsertion.gc`
`span_coe` 📖	mathematical	—	`span` `SetLike.coe` `Projectivization.Subspace` `Projectivization` `Field.toDivisionRing` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`span_empty` 📖	mathematical	—	`span` `Set` `Projectivization` `Field.toDivisionRing` `Set.instEmptyCollection` `Bot.bot` `Projectivization.Subspace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`span_eq_of_le` 📖	—	`Set` `Projectivization` `Field.toDivisionRing` `Set.instHasSubset` `SetLike.coe` `Projectivization.Subspace` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span`	—	—	`le_antisymm` `span_le_subspace_iff`
`span_eq_sInf` 📖	mathematical	—	`span` `InfSet.sInf` `Projectivization.Subspace` `instInfSet` `setOf` `Set` `Projectivization` `Field.toDivisionRing` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`ext` `Set.ext` `mem_span` `sInf_le`
`span_eq_span_iff` 📖	mathematical	—	`span` `Set` `Projectivization` `Field.toDivisionRing` `Set.instHasSubset` `SetLike.coe` `Projectivization.Subspace` `instSetLike`	—	`subset_span` `le_antisymm` `span_le_subspace_iff`
`span_iUnion` 📖	mathematical	—	`span` `Set.iUnion` `Projectivization` `Field.toDivisionRing` `iSup` `Projectivization.Subspace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`span_le_span` 📖	mathematical	`Set` `Projectivization` `Field.toDivisionRing` `Set.instHasSubset`	`Projectivization.Subspace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span`	—	`monotone_span`
`span_le_subspace_iff` 📖	mathematical	—	`Projectivization.Subspace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span` `Set` `Projectivization` `Field.toDivisionRing` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`GaloisInsertion.gc`
`span_sup` 📖	mathematical	—	`Projectivization.Subspace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `span` `Set` `Projectivization` `Field.toDivisionRing` `Set.instUnion` `SetLike.coe` `instSetLike`	—	`span_union` `span_coe`
`span_union` 📖	mathematical	—	`span` `Set` `Projectivization` `Field.toDivisionRing` `Set.instUnion` `Projectivization.Subspace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`span_univ` 📖	mathematical	—	`span` `Set.univ` `Projectivization` `Field.toDivisionRing` `Top.top` `Projectivization.Subspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`eq_top_iff` `SetLike.le_def` `instIsConcreteLE` `subset_span` `Set.mem_univ`
`subset_span` 📖	mathematical	—	`Set` `Projectivization` `Field.toDivisionRing` `Set.instHasSubset` `SetLike.coe` `Projectivization.Subspace` `instSetLike` `span`	—	—
`subset_span_trans` 📖	—	`Set` `Projectivization` `Field.toDivisionRing` `Set.instHasSubset` `SetLike.coe` `Projectivization.Subspace` `instSetLike` `span`	—	—	`GaloisConnection.le_u_l_trans` `GaloisInsertion.gc`
`sup_span` 📖	mathematical	—	`Projectivization.Subspace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `span` `Set` `Projectivization` `Field.toDivisionRing` `Set.instUnion` `SetLike.coe` `instSetLike`	—	`span_union` `span_coe`

Submodule

Definitions

Name	Category	Theorems
`projectivization` 📖	CompOp	2 math math: `mk_mem_projectivization_iff`, `mem_projectivization_iff_submodule_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_projectivization_iff_submodule_le` 📖	mathematical	—	`Projectivization` `Field.toDivisionRing` `Projectivization.Subspace` `SetLike.instMembership` `Projectivization.Subspace.instSetLike` `DFunLike.coe` `OrderIso` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Projectivization.Subspace.instPartialOrder` `instFunLikeOrderIso` `projectivization` `DivisionRing.toDivisionSemiring` `Projectivization.submodule`	—	`Projectivization.ind` `mk_mem_projectivization_iff` `span_singleton_le_iff_mem`
`mk_mem_projectivization_iff` 📖	mathematical	—	`Projectivization` `Field.toDivisionRing` `Projectivization.Subspace` `SetLike.instMembership` `Projectivization.Subspace.instSetLike` `DFunLike.coe` `OrderIso` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Projectivization.Subspace.instPartialOrder` `instFunLikeOrderIso` `projectivization` `setLike`	—	—

(root)

Definitions

Name	Category	Theorems
`Subspace` 📖	CompOp	20 math math: `Subspace.dualLift_of_subtype`, `Subspace.dualRestrict_comp_dualLift`, `Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff`, `Subspace.dualRestrict_leftInverse`, `Subspace.quotAnnihilatorEquiv_apply`, `Subspace.finrank_add_finrank_dualCoannihilator_eq`, `Subspace.dualAnnihilator_iInf_eq`, `Subspace.dualEquivDual_def`, `Subspace.dualLift_rightInverse`, `Subspace.dualLift_injective`, `exists_extension_norm_eq`, `Subspace.dualAnnihilator_le_dualAnnihilator_iff`, `LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal`, `LinearMap.BilinForm.finrank_add_finrank_orthogonal`, `Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl`, `Real.exists_extension_norm_eq`, `Subspace.dualAnnihilator_inf_eq`, `Subspace.finrank_add_finrank_dualAnnihilator_eq`, `Subspace.dualPairing_eq`, `Subspace.dualEquivDual_apply`

---

← Back to Index