Documentation Verification Report

Set

📁 Source: Mathlib/Order/Hom/Set.lean

Statistics

Metric	Count
Definitions `orderIso`, `Ici`, `Iic`, `univ`, `compl`, `setCongr`, `unique_of_wellFoundedGT`, `unique_of_wellFoundedLT`, `sumEquiv`, `orderIso`, `orderIsoOfSurjective`, `orderIso`	12
Theorems `orderIso_apply`, `range_inj`, `compl_apply`, `compl_symm_apply`, `image_eq_preimage_symm`, `image_preimage`, `image_symm_image`, `preimage_image`, `preimage_symm_preimage`, `range_eq`, `setCongr_apply`, `setCongr_symm_apply`, `subsingleton_of_wellFoundedGT`, `subsingleton_of_wellFoundedGT'`, `subsingleton_of_wellFoundedLT`, `subsingleton_of_wellFoundedLT'`, `symm_image_image`, `symm_preimage_preimage`, `sumElim`, `sumElim`, `sumEquiv_apply`, `sumEquiv_symm_apply`, `coe_orderIsoOfSurjective`, `orderIsoOfSurjective_self_symm_apply`, `orderIsoOfSurjective_symm_apply_self`, `orderIso_apply`, `compl_antitone`, `compl_strictAnti`	28
Total	40

OrderEmbedding

Definitions

Name	Category	Theorems
`orderIso` 📖	CompOp	1 math math: `orderIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Set.Elem` `Set.range` `OrderEmbedding` `instFunLikeOrderEmbedding` `Set` `Set.instMembership` `RelIso.instFunLike` `orderIso` `RelEmbedding` `RelEmbedding.instFunLike`	—	—
`range_inj` 📖	mathematical	—	`Set.range` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding`	—	`strictMono` `DFunLike.coe_fn_eq`

OrderIso

Definitions

Name	Category	Theorems
`Ici` 📖	CompOp	—
`Iic` 📖	CompOp	—
`compl` 📖	CompOp	2 math math: `compl_symm_apply`, `compl_apply`
`setCongr` 📖	CompOp	5 math math: `IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal`, `IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe`, `Set.powersetCard.orderIsoOfFin_symm_apply_val`, `setCongr_symm_apply`, `setCongr_apply`
`unique_of_wellFoundedGT` 📖	CompOp	—
`unique_of_wellFoundedLT` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `OrderDual.instLE` `RelIso.instFunLike` `compl` `Compl.compl` `BooleanAlgebra.toCompl` `OrderDual.instBooleanAlgebra` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`compl_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `RelIso.instFunLike` `RelIso.symm` `compl` `Compl.compl` `BooleanAlgebra.toCompl` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`image_eq_preimage_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `Set.preimage` `symm`	—	`Equiv.image_eq_preimage_symm`
`image_preimage` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `Set.preimage`	—	`Equiv.image_preimage`
`image_symm_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `symm`	—	`Equiv.image_symm_image`
`preimage_image` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `Set.image`	—	`Equiv.preimage_image`
`preimage_symm_preimage` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `symm`	—	`Equiv.preimage_symm_preimage`
`range_eq` 📖	mathematical	—	`Set.range` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `Set.univ`	—	`Function.Surjective.range_eq` `surjective`
`setCongr_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Set.Elem` `Preorder.toLE` `Set` `Set.instMembership` `RelIso.instFunLike` `setCongr` `Equiv.refl`	—	—
`setCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Set.Elem` `Preorder.toLE` `Set` `Set.instMembership` `RelIso.instFunLike` `RelIso.symm` `setCongr` `Equiv.refl`	—	—
`subsingleton_of_wellFoundedGT` 📖	mathematical	—	`OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`subsingleton_of_wellFoundedLT` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`subsingleton_of_wellFoundedGT'` 📖	mathematical	—	`OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`subsingleton_of_wellFoundedLT'` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`subsingleton_of_wellFoundedLT` 📖	mathematical	—	`OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`ext_iff` `coe_toOrderEmbedding` `DFunLike.coe_fn_eq` `range_eq`
`subsingleton_of_wellFoundedLT'` 📖	mathematical	—	`OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`subsingleton_of_wellFoundedLT`
`symm_image_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `symm`	—	`Equiv.symm_image_image`
`symm_preimage_preimage` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `symm`	—	`Equiv.symm_preimage_preimage`

OrderIso.Set

Definitions

Name	Category	Theorems
`univ` 📖	CompOp	—

Set

Definitions

Name	Category	Theorems
`sumEquiv` 📖	CompOp	6 math math: `sumEquiv_apply`, `InjOn.sumElim`, `sumEquiv_symm_apply`, `ncard_sumEquiv_symm_apply`, `NumberField.InfinitePlace.bijOn_sumElim_conjugate`, `MapsTo.sumElim`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Set` `instLE` `Prod.instLE_mathlib` `RelIso.instFunLike` `sumEquiv` `preimage`	—	—
`sumEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Set` `Prod.instLE_mathlib` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `sumEquiv` `instUnion` `image`	—	—

Set.InjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumElim` 📖	mathematical	`Set.InjOn` `Set`	`Set.InjOn` `DFunLike.coe` `OrderIso` `Set` `Prod.instLE_mathlib` `Set.instLE` `instFunLikeOrderIso` `OrderIso.symm` `Set.sumEquiv`	—	—

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumElim` 📖	mathematical	`Set.MapsTo` `Set`	`Set.MapsTo` `DFunLike.coe` `OrderIso` `Set` `Prod.instLE_mathlib` `Set.instLE` `instFunLikeOrderIso` `OrderIso.symm` `Set.sumEquiv`	—	—

StrictMono

Definitions

Name	Category	Theorems
`orderIso` 📖	CompOp	1 math math: `orderIso_apply`
`orderIsoOfSurjective` 📖	CompOp	3 math math: `orderIsoOfSurjective_symm_apply_self`, `orderIsoOfSurjective_self_symm_apply`, `coe_orderIsoOfSurjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_orderIsoOfSurjective` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderIso` `orderIsoOfSurjective`	—	—
`orderIsoOfSurjective_self_symm_apply` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoOfSurjective`	—	`OrderIso.apply_symm_apply`
`orderIsoOfSurjective_symm_apply_self` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoOfSurjective`	—	`OrderIso.symm_apply_apply`
`orderIso_apply` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `RelIso` `Set.Elem` `Set.range` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership` `RelIso.instFunLike` `orderIso`	—	—

StrictMonoOn

Definitions

Name	Category	Theorems
`orderIso` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_antitone` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl`	—	`OrderIso.monotone`
`compl_strictAnti` 📖	mathematical	—	`StrictAnti` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl`	—	`OrderIso.strictMono`

---

← Back to Index