Documentation Verification Report

Set

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

Statistics

Metric	Count
Definitions `codRestrict`, `subrelUnivIso`, `Subrel`, `inclusionEmbedding`, `relEmbedding`	5
Theorems `of_subrel`, `codRestrict_apply`, `directed`, `directedOn`, `map_inf`, `map_sup`, `image_eq_preimage_symm`, `preimage_eq_image_symm`, `range_eq`, `subrelUnivIso_apply`, `subrelUnivIso_symm_apply`, `coe_inclusionEmbedding`, `instAsymmSubtype`, `instIrreflSubtype`, `instIsPreorderSubtype`, `instIsStrictOrderSubtype`, `instIsTransSubtype`, `instIsWellFoundedSubtype`, `instIsWellOrderSubtype`, `instReflSubtype`, `instSymmSubtype`, `instTrichotomousSubtype`, `relEmbedding_apply`, `subrel_val`, `wellFounded_iff_wellFounded_subrel`	25
Total	30

Acc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_subrel` 📖	—	`Subrel`	—	—	`trans`

RelEmbedding

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	1 math math: `codRestrict_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codRestrict_apply` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `RelEmbedding` `instFunLike`	`Subrel` `codRestrict`	—	—

RelHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed` 📖	mathematical	`Directed`	`DFunLike.coe`	—	`Directed.mono_comp` `map_rel`
`directedOn` 📖	mathematical	`DirectedOn`	`Set.image` `DFunLike.coe`	—	`DirectedOn.mono_comp` `map_rel`
`map_inf` 📖	mathematical	—	`DFunLike.coe` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.map_inf` `StrictMono.monotone` `map_rel`
`map_sup` 📖	mathematical	—	`DFunLike.coe` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`map_inf`

RelIso

Definitions

Name	Category	Theorems
`subrelUnivIso` 📖	CompOp	2 math math: `subrelUnivIso_symm_apply`, `subrelUnivIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_eq_preimage_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `RelIso` `instFunLike` `Set.preimage` `symm`	—	`Equiv.image_eq_preimage_symm`
`preimage_eq_image_symm` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `RelIso` `instFunLike` `Set.image` `symm`	—	`image_eq_preimage_symm`
`range_eq` 📖	mathematical	—	`Set.range` `DFunLike.coe` `RelIso` `instFunLike` `Set.univ`	—	`EquivLike.range_eq_univ`
`subrelUnivIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrel` `instFunLike` `subrelUnivIso`	—	—
`subrelUnivIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrel` `instFunLike` `symm` `subrelUnivIso`	—	—

Subrel

Definitions

Name	Category	Theorems
`inclusionEmbedding` 📖	CompOp	1 math math: `coe_inclusionEmbedding`
`relEmbedding` 📖	CompOp	1 math math: `relEmbedding_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inclusionEmbedding` 📖	mathematical	`Set` `Set.instHasSubset`	`DFunLike.coe` `RelEmbedding` `Set.instMembership` `Subrel` `RelEmbedding.instFunLike` `inclusionEmbedding` `Set.inclusion`	—	—
`instAsymmSubtype` 📖	mathematical	—	`Subrel`	—	—
`instIrreflSubtype` 📖	mathematical	—	`Subrel`	—	—
`instIsPreorderSubtype` 📖	mathematical	—	`IsPreorder` `Subrel`	—	`instReflSubtype` `IsPreorder.toRefl` `instIsTransSubtype` `IsPreorder.toIsTrans`
`instIsStrictOrderSubtype` 📖	mathematical	—	`IsStrictOrder` `Subrel`	—	`instIrreflSubtype` `IsStrictOrder.toIrrefl` `instIsTransSubtype` `IsStrictOrder.toIsTrans`
`instIsTransSubtype` 📖	mathematical	—	`IsTrans` `Subrel`	—	`IsTrans.trans`
`instIsWellFoundedSubtype` 📖	mathematical	—	`IsWellFounded` `Subrel`	—	`RelEmbedding.isWellFounded`
`instIsWellOrderSubtype` 📖	mathematical	—	`IsWellOrder` `Subrel`	—	`instTrichotomousSubtype` `IsWellOrder.toTrichotomous` `instIsTransSubtype` `IsWellOrder.toIsTrans` `instIsWellFoundedSubtype` `IsWellOrder.toIsWellFounded`
`instReflSubtype` 📖	mathematical	—	`Subrel`	—	—
`instSymmSubtype` 📖	mathematical	—	`Subrel`	—	—
`instTrichotomousSubtype` 📖	mathematical	—	`Subrel`	—	—
`relEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Subrel` `RelEmbedding.instFunLike` `relEmbedding`	—	—

(root)

Definitions

Name	Category	Theorems
`Subrel` 📖	MathDef	40 math math: `Subrel.instAsymmSubtype`, `RelIso.sumLexComplRight_apply`, `Subrel.instSymmSubtype`, `PrincipalSeg.codRestrict_apply`, `RelIso.sumLexComplLeft_symm_apply`, `ZFSet.IsOrdinal.trichotomous`, `subrel_val`, `PrincipalSeg.codRestrict_top`, `PrincipalSeg.apply_subrelIso`, `RelIso.subrelUnivIso_symm_apply`, `Subrel.instIrreflSubtype`, `PrincipalSeg.ofElement_top`, `Ordinal.type_subrel`, `ZFSet.IsOrdinal.isTrichotomous`, `Subrel.relEmbedding_apply`, `Subrel.instIsWellOrderSubtype`, `Subrel.instReflSubtype`, `ZFSet.IsOrdinal.isTrans`, `PrincipalSeg.ofElement_apply`, `PrincipalSeg.subrelIso_symm_apply`, `ZFSet.IsOrdinal.isWellOrder`, `RelIso.sumLexComplRight_symm_apply`, `Subrel.instIsStrictOrderSubtype`, `ZFSet.isOrdinal_iff_isTrans`, `Subrel.instIsWellFoundedSubtype`, `Ordinal.ord_cof_eq`, `Subrel.instTrichotomousSubtype`, `Subrel.instIsTransSubtype`, `ZFSet.isOrdinal_iff_isTrichotomous`, `ZFSet.isOrdinal_iff_trichotomous`, `RelEmbedding.codRestrict_apply`, `RelIso.sumLexComplLeft_apply`, `ZFSet.isOrdinal_iff_isWellOrder`, `RelIso.subrelUnivIso_apply`, `InitialSeg.codRestrict_apply`, `wellFounded_iff_wellFounded_subrel`, `Subrel.instIsPreorderSubtype`, `PrincipalSeg.subrelIso_apply`, `Subrel.coe_inclusionEmbedding`, `PrincipalSeg.ofElement_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subrel_val` 📖	mathematical	—	`Subrel`	—	—
`wellFounded_iff_wellFounded_subrel` 📖	mathematical	—	`Subrel`	—	`Acc.of_subrel`

---

← Back to Index