Documentation Verification Report

DirectedInverseSystem

📁 Source: Mathlib/Order/DirectedInverseSystem.lean

Statistics

Metric	Count
Definitions `lift₂`, `map`, `map₀`, `map₂`, `setoid`, `DirectedSystem`, `InverseSystem`, `IsNatEquiv`, `PEquivOn`, `equiv`, `restrict`, `globalEquiv`, `invLimEquiv`, `limit`, `pEquivOnGlue`, `pEquivOnLim`, `pEquivOnSucc`, `piEquivLim`, `piEquivSucc`, `piLT`, `piLTLim`, `piLTProj`, `piSplitLE`	23
Theorems `eq_of_le`, `exists_eq_mk`, `exists_eq_mk₂`, `exists_eq_mk₃`, `induction`, `induction₂`, `induction₃`, `lift_def`, `lift_injective`, `lift₂_def`, `lift₂_def₂`, `map_def`, `map₀_def`, `map₂_def`, `map₂_def₂`, `mk_injective`, `r_of_le`, `map_map`, `map_map'`, `map_self`, `map_self'`, `compat`, `ext`, `ext_iff`, `nat`, `restrict_equiv`, `globalEquiv_compatibility`, `globalEquiv_naturality`, `invLimEquiv_apply_coe`, `invLimEquiv_symm_apply_coe`, `isNatEquiv_piEquivLim`, `isNatEquiv_piEquivSucc`, `map_map`, `map_self`, `pEquivOn_apply_eq`, `piEquivSucc_self`, `piLTLim_apply`, `piLTLim_symm_apply`, `piLTProj_intro`, `piSplitLE_eq`, `piSplitLE_lt`, `unique_pEquivOn`	42
Total	65

DirectLimit

Definitions

Name	Category	Theorems
`lift₂` 📖	CompOp	2 math math: `lift₂_def₂`, `lift₂_def`
`map` 📖	CompOp	1 math math: `map_def`
`map₀` 📖	CompOp	1 math math: `map₀_def`
`map₂` 📖	CompOp	2 math math: `map₂_def₂`, `map₂_def`
`setoid` 📖	CompOp	40 math math: `zsmul_def`, `zpow₀_def`, `map_def`, `exists_eq_mk₂`, `lift₂_def₂`, `map₂_def₂`, `ratCast_def`, `lift_def`, `lift₂_def`, `nsmul_def`, `vadd_def`, `neg_def`, `mul_def`, `natCast_def`, `Module.DirectLimit.linearEquiv_of`, `exists_eq_one`, `intCast_def`, `add_def`, `exists_eq_mk`, `smul_def`, `zpow_def`, `Module.DirectLimit.linearEquiv_symm_mk`, `Ring.DirectLimit.ringEquiv_of`, `exists_eq_zero`, `one_def`, `inv₀_def`, `mk_injective`, `map₂_def`, `npow_def`, `Ring.DirectLimit.ringEquiv_symm_mk`, `eq_of_le`, `r_of_le`, `div₀_def`, `zero_def`, `nnratCast_def`, `sub_def`, `inv_def`, `map₀_def`, `exists_eq_mk₃`, `div_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_le` 📖	mathematical	`Preorder.toLE`	`setoid` `DFunLike.coe`	—	`r_of_le`
`exists_eq_mk` 📖	mathematical	—	`setoid`	—	—
`exists_eq_mk₂` 📖	mathematical	—	`setoid`	—	`exists_ge_ge` `eq_of_le`
`exists_eq_mk₃` 📖	mathematical	—	`setoid`	—	`directed_of₃` `instIsTransLe` `eq_of_le`
`induction` 📖	—	`setoid`	—	—	—
`induction₂` 📖	—	`setoid`	—	—	`exists_eq_mk₂`
`induction₃` 📖	—	`setoid`	—	—	`exists_eq_mk₃`
`lift_def` 📖	mathematical	`DFunLike.coe`	`lift` `setoid`	—	—
`lift_injective` 📖	mathematical	`DFunLike.coe`	`DirectLimit` `lift`	—	`induction₂`
`lift₂_def` 📖	mathematical	`DFunLike.coe`	`lift₂` `setoid`	—	`le_rfl` `lift₂_def₂` `DirectedSystem.map_self'`
`lift₂_def₂` 📖	mathematical	`DFunLike.coe` `Preorder.toLE`	`lift₂` `setoid`	—	—
`map_def` 📖	mathematical	`DFunLike.coe`	`map` `setoid`	—	—
`map₀_def` 📖	mathematical	`DFunLike.coe`	`map₀` `setoid`	—	`exists_ge_ge`
`map₂_def` 📖	mathematical	`DFunLike.coe`	`map₂` `setoid`	—	`lift₂_def`
`map₂_def₂` 📖	mathematical	`DFunLike.coe` `Preorder.toLE`	`map₂` `setoid`	—	`lift₂_def₂`
`mk_injective` 📖	mathematical	`DFunLike.coe`	`setoid`	—	`Quotient.eq`
`r_of_le` 📖	mathematical	`Preorder.toLE`	`setoid` `DFunLike.coe`	—	`le_rfl` `LE.le.trans` `DirectedSystem.map_map'`

DirectedSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_map` 📖	mathematical	`Preorder.toLE`	`LE.le.trans`	—	—
`map_map'` 📖	mathematical	`Preorder.toLE`	`DFunLike.coe` `LE.le.trans`	—	`map_map`
`map_self` 📖	mathematical	—	`le_rfl`	—	—
`map_self'` 📖	mathematical	—	`DFunLike.coe` `le_rfl`	—	`map_self`

InverseSystem

Definitions

Name	Category	Theorems
`IsNatEquiv` 📖	MathDef	1 math math: `PEquivOn.nat`
`PEquivOn` 📖	CompData	—
`globalEquiv` 📖	CompOp	2 math math: `globalEquiv_compatibility`, `globalEquiv_naturality`
`invLimEquiv` 📖	CompOp	2 math math: `invLimEquiv_apply_coe`, `invLimEquiv_symm_apply_coe`
`limit` 📖	CompOp	5 math math: `Field.Emb.Cardinal.equivLim_coherence`, `invLimEquiv_apply_coe`, `piLTLim_symm_apply`, `invLimEquiv_symm_apply_coe`, `piLTLim_apply`
`pEquivOnGlue` 📖	CompOp	—
`pEquivOnLim` 📖	CompOp	—
`pEquivOnSucc` 📖	CompOp	—
`piEquivLim` 📖	CompOp	1 math math: `isNatEquiv_piEquivLim`
`piEquivSucc` 📖	CompOp	2 math math: `piEquivSucc_self`, `isNatEquiv_piEquivSucc`
`piLT` 📖	CompOp	10 math math: `piEquivSucc_self`, `globalEquiv_compatibility`, `PEquivOn.compat`, `invLimEquiv_apply_coe`, `piSplitLE_eq`, `piLTLim_symm_apply`, `piSplitLE_lt`, `globalEquiv_naturality`, `invLimEquiv_symm_apply_coe`, `piLTLim_apply`
`piLTLim` 📖	CompOp	2 math math: `piLTLim_symm_apply`, `piLTLim_apply`
`piLTProj` 📖	CompOp	6 math math: `piLTProj_intro`, `invLimEquiv_apply_coe`, `piLTLim_symm_apply`, `globalEquiv_naturality`, `invLimEquiv_symm_apply_coe`, `piLTLim_apply`
`piSplitLE` 📖	CompOp	2 math math: `piSplitLE_eq`, `piSplitLE_lt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`globalEquiv_compatibility` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `Equiv` `Order.succ` `piLT` `EquivLike.toFunLike` `Equiv.instEquivLike` `globalEquiv` `Set` `Set.instMembership` `Set.Iio` `Order.lt_succ_of_not_isMax`	—	`Order.le_succ` `LT.lt.le` `PEquivOn.compat` `le_rfl`
`globalEquiv_naturality` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `Equiv` `piLT` `EquivLike.toFunLike` `Equiv.instEquivLike` `globalEquiv` `piLTProj`	—	`Order.le_succ` `LT.lt.le` `DFunLike.congr_fun` `pEquivOn_apply_eq` `IsLowerSet.inter` `isLowerSet_Iic` `PEquivOn.nat` `le_rfl`
`invLimEquiv_apply_coe` 📖	mathematical	`IsNatEquiv` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iio`	`Set` `Set.instMembership` `limit` `piLT` `piLTProj` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `invLimEquiv`	—	—
`invLimEquiv_symm_apply_coe` 📖	mathematical	`IsNatEquiv` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iio`	`Set` `Set.instMembership` `limit` `DFunLike.coe` `Equiv` `Set.Elem` `piLT` `piLTProj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `invLimEquiv`	—	—
`isNatEquiv_piEquivLim` 📖	mathematical	`IsNatEquiv` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iio` `Order.IsSuccPrelimit` `Preorder.toLT` `Set` `Set.instMembership` `limit` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `LT.lt.le`	`Set.Iic` `piEquivLim`	—	`LT.lt.le` `LE.le.eq_or_lt` `map_self` `piSplitLE_lt` `piLTProj.congr_simp` `piSplitLE_eq` `piLTProj.eq_1` `piLTLim_symm_apply` `invLimEquiv_apply_coe` `piEquivLim.eq_1` `LE.le.trans_lt`
`isNatEquiv_piEquivSucc` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `Order.succ` `EquivLike.toFunLike` `Equiv.instEquivLike` `Order.le_succ` `IsNatEquiv` `Set.Iic`	`piEquivSucc`	—	`Order.le_succ` `Order.lt_succ_iff_of_not_isMax` `Order.le_succ_iff_eq_or_le` `map_self` `piEquivSucc.eq_1` `LT.lt.le` `piSplitLE_lt` `LE.le.trans` `map_map` `piLTProj.eq_1` `le_rfl` `LT.lt.trans_le` `piSplitLE_eq` `LE.le.trans_lt`
`map_map` 📖	mathematical	`Preorder.toLE`	`LE.le.trans`	—	—
`map_self` 📖	mathematical	—	`le_rfl`	—	—
`pEquivOn_apply_eq` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instInter` `Set.instMembership`	`PEquivOn.equiv`	—	`Set.inter_subset_left` `Set.inter_subset_right` `unique_pEquivOn`
`piEquivSucc_self` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `Equiv` `Set` `Set.instMembership` `Set.Iic` `Order.succ` `le_rfl` `piLT` `EquivLike.toFunLike` `Equiv.instEquivLike` `piEquivSucc` `Set.Iio` `Order.lt_succ_of_not_isMax`	—	`le_rfl` `Order.lt_succ_of_not_isMax` `piSplitLE_eq`
`piLTLim_apply` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `Equiv` `piLT` `Set.Elem` `limit` `piLTProj` `EquivLike.toFunLike` `Equiv.instEquivLike` `piLTLim` `Set` `Set.instMembership` `Set.Iio`	—	—
`piLTLim_symm_apply` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership` `Set.Iio`	`DFunLike.coe` `Equiv` `Set.Elem` `limit` `piLT` `piLTProj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `piLTLim`	—	`Equiv.right_inv`
`piLTProj_intro` 📖	mathematical	`Preorder.toLE` `Preorder.toLT` `Set` `Set.instMembership` `Set.Iio`	`piLTProj`	—	—
`piSplitLE_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `piLT` `PartialOrder.toPreorder` `EquivLike.toFunLike` `Equiv.instEquivLike` `piSplitLE` `Set` `Set.instMembership` `Set.Iic` `le_rfl`	—	`le_rfl`
`piSplitLE_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`DFunLike.coe` `Equiv` `piLT` `EquivLike.toFunLike` `Equiv.instEquivLike` `piSplitLE` `Set` `Set.instMembership` `Set.Iic` `LT.lt.le` `Set.Iio`	—	`LT.lt.le` `LT.lt.ne`
`unique_pEquivOn` 📖	—	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`Order.lt_succ_of_not_isMax` `PEquivOn.ext` `Equiv.ext` `LE.le.eq_or_lt` `Order.lt_succ_iff_of_not_isMax` `Order.le_succ` `piLTProj_intro` `LT.lt.le`

InverseSystem.PEquivOn

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	5 math math: `restrict_equiv`, `compat`, `nat`, `ext_iff`, `InverseSystem.pEquivOn_apply_eq`
`restrict` 📖	CompOp	1 math math: `restrict_equiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compat` 📖	mathematical	`Set` `Set.instMembership` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsMax` `Preorder.toLE`	`DFunLike.coe` `Equiv` `InverseSystem.piLT` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `Set.Iio` `Order.lt_succ_of_not_isMax`	—	—
`ext` 📖	—	`equiv`	—	—	`Order.lt_succ_of_not_isMax`
`ext_iff` 📖	mathematical	—	`equiv`	—	`ext`
`nat` 📖	mathematical	—	`InverseSystem.IsNatEquiv` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `equiv`	—	—
`restrict_equiv` 📖	mathematical	`Set` `Set.instHasSubset`	`equiv` `restrict` `Set.instMembership`	—	—

(root)

Definitions

Name	Category	Theorems
`DirectedSystem` 📖	CompData	13 math math: `Submodule.FG.rTensor.directedSystem`, `Submodule.FG.lTensor.directedSystem`, `TensorProduct.instDirectedSystemCoeLinearMapIdRTensor`, `DirectedSystem.lTensor`, `AddCommGroup.DirectLimit.directedSystem`, `DirectedSystem.rTensor`, `Submodule.FG.directedSystem`, `FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion`, `FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion`, `FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion`, `Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId`, `TensorProduct.instDirectedSystemCoeLinearMapIdLTensor`, `FirstOrder.Language.DirectedSystem.natLERec.directedSystem`
`InverseSystem` 📖	CompData	1 math math: `Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor`

---

← Back to Index