Documentation Verification Report

Set

📁 Source: Mathlib/Logic/Embedding/Set.lean

Statistics

Metric	Count
Definitions `codRestrict`, `image`, `optionElim`, `optionEmbeddingEquiv`, `sigmaSet`, `sumSet`, `embeddingOfSubset`, `subtypeOrEquiv`	8
Theorems `asEmbedding_range`, `codRestrict_apply`, `coe_sigmaSet`, `coe_sumSet`, `image_apply`, `optionElim_apply`, `optionEmbeddingEquiv_apply_fst`, `optionEmbeddingEquiv_apply_snd_coe`, `optionEmbeddingEquiv_symm_apply`, `sigmaSet_apply`, `sigmaSet_preimage`, `sigmaSet_range`, `sumSet_apply`, `sumSet_preimage_inl`, `sumSet_preimage_inr`, `sumSet_range`, `embeddingOfSubset_apply_coe`, `subtypeOrEquiv_apply`, `subtypeOrEquiv_symm_inl`, `subtypeOrEquiv_symm_inr`	20
Total	28

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asEmbedding_range` 📖	mathematical	—	`Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `asEmbedding` `setOf`	—	`Set.ext` `Subtype.coe_prop` `apply_symm_apply`

Function.Embedding

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	1 math math: `codRestrict_apply`
`image` 📖	CompOp	1 math math: `image_apply`
`optionElim` 📖	CompOp	2 math math: `optionElim_apply`, `optionEmbeddingEquiv_symm_apply`
`optionEmbeddingEquiv` 📖	CompOp	3 math math: `optionEmbeddingEquiv_apply_snd_coe`, `optionEmbeddingEquiv_symm_apply`, `optionEmbeddingEquiv_apply_fst`
`sigmaSet` 📖	CompOp	4 math math: `sigmaSet_apply`, `coe_sigmaSet`, `sigmaSet_range`, `sigmaSet_preimage`
`sumSet` 📖	CompOp	5 math math: `sumSet_apply`, `sumSet_range`, `sumSet_preimage_inr`, `sumSet_preimage_inl`, `coe_sumSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codRestrict_apply` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`Set.Elem` `codRestrict`	—	—
`coe_sigmaSet` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`DFunLike.coe` `Function.Embedding` `Set.Elem` `Function.instFunLikeEmbedding` `sigmaSet` `Set.instMembership`	—	—
`coe_sumSet` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`DFunLike.coe` `Function.Embedding` `Set.Elem` `Function.instFunLikeEmbedding` `sumSet` `Set.instMembership`	—	—
`image_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Set` `Function.instFunLikeEmbedding` `image` `Set.image`	—	—
`optionElim_apply` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`optionElim` `Option.elim'`	—	—
`optionEmbeddingEquiv_apply_fst` 📖	mathematical	—	`Function.Embedding` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.range` `DFunLike.coe` `Function.instFunLikeEmbedding` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `optionEmbeddingEquiv` `trans` `some`	—	—
`optionEmbeddingEquiv_apply_snd_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Compl.compl` `Set.instCompl` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `trans` `some` `Set.Elem` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `optionEmbeddingEquiv`	—	—
`optionEmbeddingEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Function.Embedding` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.range` `Function.instFunLikeEmbedding` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `optionEmbeddingEquiv` `optionElim` `Set.instMembership`	—	—
`sigmaSet_apply` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`DFunLike.coe` `Function.Embedding` `Set.Elem` `Function.instFunLikeEmbedding` `sigmaSet` `Set.instMembership`	—	—
`sigmaSet_preimage` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`Set.image` `Set.instMembership` `Set.preimage` `Set.Elem` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `sigmaSet` `Set.instInter`	—	—
`sigmaSet_range` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`Set.range` `Set.Elem` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `sigmaSet` `Set.iUnion`	—	—
`sumSet_apply` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`DFunLike.coe` `Function.Embedding` `Set.Elem` `Function.instFunLikeEmbedding` `sumSet` `Set.instMembership`	—	—
`sumSet_preimage_inl` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`Set.image` `Set.instMembership` `Set.preimage` `Set.Elem` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `sumSet` `Set.instInter`	—	—
`sumSet_preimage_inr` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`Set.image` `Set.instMembership` `Set.preimage` `Set.Elem` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `sumSet` `Set.instInter`	—	—
`sumSet_range` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`Set.range` `Set.Elem` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `sumSet` `Set.instUnion`	—	—

Set

Definitions

Name	Category	Theorems
`embeddingOfSubset` 📖	CompOp	1 math math: `embeddingOfSubset_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embeddingOfSubset_apply_coe` 📖	mathematical	`Set` `instHasSubset`	`instMembership` `DFunLike.coe` `Function.Embedding` `Elem` `Function.instFunLikeEmbedding` `embeddingOfSubset`	—	—

(root)

Definitions

Name	Category	Theorems
`subtypeOrEquiv` 📖	CompOp	3 math math: `subtypeOrEquiv_symm_inl`, `subtypeOrEquiv_symm_inr`, `subtypeOrEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subtypeOrEquiv_apply` 📖	mathematical	`Disjoint` `Pi.partialOrder` `Prop.partialOrder` `Pi.instOrderBot` `Prop.le` `HeytingAlgebra.toOrderBot` `Prop.instHeytingAlgebra`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `subtypeOrEquiv` `Function.Embedding` `Function.instFunLikeEmbedding` `subtypeOrLeftEmbedding`	—	—
`subtypeOrEquiv_symm_inl` 📖	mathematical	`Disjoint` `Pi.partialOrder` `Prop.partialOrder` `Pi.instOrderBot` `Prop.le` `HeytingAlgebra.toOrderBot` `Prop.instHeytingAlgebra`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `subtypeOrEquiv` `Subtype.prop`	—	—
`subtypeOrEquiv_symm_inr` 📖	mathematical	`Disjoint` `Pi.partialOrder` `Prop.partialOrder` `Pi.instOrderBot` `Prop.le` `HeytingAlgebra.toOrderBot` `Prop.instHeytingAlgebra`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `subtypeOrEquiv` `Subtype.prop`	—	—

---

← Back to Index