Documentation Verification Report

PowersetCard

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

Statistics

Metric	Count
Definitions `ofFinEmbEquiv`	1
Theorems `mem_ofFinEmbEquiv_iff_mem_range`, `mem_range_ofFinEmbEquiv_symm_iff_mem`, `ofFinEmbEquiv_apply`, `ofFinEmbEquiv_symm_apply`	4
Total	5

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`

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`	—	—

---

← Back to Index