Documentation Verification Report

PowersetCard

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

Statistics

Metric	Count
Definitions `ofFinEmbEquiv`, `orderIsoOfFin`, `permOfDisjoint`	3
Theorems `mem_ofFinEmbEquiv_iff_mem_range`, `mem_range_ofFinEmbEquiv_symm_iff_mem`, `ofFinEmbEquiv_apply`, `ofFinEmbEquiv_symm_apply`, `orderIsoOfFin_apply_coe`, `orderIsoOfFin_symm_apply_val`	6
Total	9

Set.powersetCard

Definitions

Name	Category	Theorems
`ofFinEmbEquiv` 📖	CompOp	5 math math: `ofFinEmbEquiv_symm_apply`, `exteriorPower.ιMultiDual_apply_ιMulti`, `mem_ofFinEmbEquiv_iff_mem_range`, `mem_range_ofFinEmbEquiv_symm_iff_mem`, `ofFinEmbEquiv_apply`
`orderIsoOfFin` 📖	CompOp	2 math math: `orderIsoOfFin_apply_coe`, `orderIsoOfFin_symm_apply_val`
`permOfDisjoint` 📖	CompOp	2 math math: `ExteriorAlgebra.basis_mul_of_disjoint`, `ExteriorAlgebra.ιMulti_family_mul_of_disjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_ofFinEmbEquiv_iff_mem_range` 📖	mathematical	—	`Set.Elem` `Finset` `Set.powersetCard` `SetLike.instMembership` `instSetLikeElemFinset` `DFunLike.coe` `Equiv` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFinEmbEquiv` `Set` `Set.instMembership` `Set.range` `instFunLikeOrderEmbedding`	—	—
`mem_range_ofFinEmbEquiv_symm_iff_mem` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `Equiv` `Set.Elem` `Finset` `Set.powersetCard` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ofFinEmbEquiv` `SetLike.instMembership` `instSetLikeElemFinset`	—	`Finset.range_orderEmbOfFin` `Subtype.prop`
`ofFinEmbEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Elem` `Finset` `Set.powersetCard` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFinEmbEquiv` `ofFinEmb` `RelEmbedding.toEmbedding`	—	—
`ofFinEmbEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `Finset` `Set.powersetCard` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ofFinEmbEquiv` `Finset.orderEmbOfFin` `Set` `Set.instMembership` `Subtype.prop`	—	—
`orderIsoOfFin_apply_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.instMembership` `Set.powersetCard` `DFunLike.coe` `RelIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelIso.instFunLike` `orderIsoOfFin` `Finset.sort` `LinearOrder.toDecidableLE` `LE.total`	—	—
`orderIsoOfFin_symm_apply_val` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.instMembership` `Set.powersetCard` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelIso.instFunLike` `RelIso.symm` `orderIsoOfFin` `LinearOrder.toDecidableEq` `Finset.sort` `LinearOrder.toDecidableLE` `LE.total` `OrderIso` `instFunLikeOrderIso` `OrderIso.symm` `OrderIso.setCongr` `setOf` `SetLike.coe` `Set.Elem` `instSetLikeElemFinset`	—	—

---

← Back to Index