PowersetCard

📁 Source: Mathlib/Data/Set/PowersetCard.lean

Statistics

Metric	Count
Definitions `powersetCard`, `compl`, `instFintypeElemFinset`, `instPartialOrderElemFinset`, `instSetLikeElemFinset`, `map`, `ofFinEmb`, `ofSingleton`	8
Theorems `card`, `card_eq`, `coe_coe`, `coe_compl`, `coe_finset`, `coe_map`, `coe_nonempty_iff`, `coe_nontrivial_iff`, `coe_ofFinEmb`, `compl_symm`, `eq_empty_iff`, `eq_iff_subset`, `exist_mem_powersetCard_of_inf`, `exists_mem_notMem`, `exists_mem_notMem_iff_ne`, `instFiniteElemFinset`, `instInfinite`, `mem_coe_iff`, `mem_compl`, `mem_iff`, `mem_map_iff_mem_range`, `mem_ofFinEmb_iff_mem_range`, `ncard_eq`, `nontrivial`, `nontrivial'`, `nontrivial_iff`, `ofFinEmb_surjective`, `val_map`, `val_ofFinEmb`	29
Total	37

Set

Definitions

Name	Category	Theorems
`powersetCard` 📖	CompOp	72 math math: `powersetCard.exist_mem_powersetCard_of_inf`, `exteriorPower.basis_apply`, `powersetCard.val_ofFinEmb`, `exteriorPower.coe_basis`, `exteriorPower.ιMulti_family_linearIndependent_field`, `powersetCard.isPretransitive`, `exteriorPower.basis_repr_ne`, `powersetCard.ofFinEmb_surjective`, `exteriorPower.ιMulti_family_span_fixedDegree_of_span`, `powersetCard.mem_mulActionHom_compl`, `powersetCard.coe_coe`, `powersetCard.faithfulSMul`, `powersetCard.compl_symm`, `powersetCard.stabilizer_coe`, `powersetCard.instInfinite`, `powersetCard.nontrivial_iff`, `powersetCard.isPretransitive_alternatingGroup`, `powersetCard.isPretransitive_of_isMultiplyPretransitive'`, `powersetCard.addAction_stabilizer_coe`, `powersetCard.addActionHom_of_embedding_surjective`, `powersetCard.exists_mem_notMem`, `powersetCard.eq_empty_iff`, `powersetCard.mem_coe_iff`, `powersetCard.coe_ofFinEmb`, `powersetCard.coe_map`, `powersetCard.mem_ofFinEmb_iff_mem_range`, `powersetCard.card_eq`, `powersetCard.ofFinEmbEquiv_symm_apply`, `powersetCard.mem_compl`, `exteriorPower.ιMultiDual_apply_ιMulti`, `exteriorPower.ιMulti_family_eq_coe_comp`, `powersetCard.mulActionHom_compl_mulActionHom_compl`, `powersetCard.coe_finset`, `powersetCard.coe_nonempty_iff`, `powersetCard.faithfulVAdd`, `powersetCard.mulActionHom_compl_bijective`, `powersetCard.addActionHom_singleton_bijective`, `powersetCard.coe_compl`, `powersetCard.mem_iff`, `exteriorPower.ιMulti_family_span_of_span`, `powersetCard.coe_addActionHom_of_embedding`, `exteriorPower.basis_coord`, `powersetCard.addAction_faithful`, `powersetCard.mem_ofFinEmbEquiv_iff_mem_range`, `powersetCard.nontrivial'`, `powersetCard.nontrivial`, `exteriorPower.basis_repr_apply`, `powersetCard.isPreprimitive_perm`, `powersetCard.isPretransitive_of_isMultiplyPretransitive`, `exteriorPower.map_comp_ιMulti_family`, `powersetCard.isPreprimitive_alternatingGroup`, `powersetCard.card`, `powersetCard.mulActionHom_singleton_bijective`, `powersetCard.mulAction_faithful`, `exteriorPower.basis_repr`, `powersetCard.coe_mulActionHom_compl`, `powersetCard.instFiniteElemFinset`, `exteriorPower.ιMulti_family_linearIndependent_ofBasis`, `powersetCard.val_map`, `powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem`, `exteriorPower.ιMulti_family_span`, `powersetCard.ncard_eq`, `powersetCard.mem_map_iff_mem_range`, `powersetCard.coe_mulActionHom_of_embedding`, `powersetCard.mulActionHom_of_embedding_surjective`, `powersetCard.coe_smul`, `powersetCard.coe_nontrivial_iff`, `powersetCard.exists_mem_notMem_iff_ne`, `exteriorPower.basis_repr_self`, `powersetCard.coe_vadd`, `powersetCard.ofFinEmbEquiv_apply`, `powersetCard.eq_iff_subset`

Set.powersetCard

Definitions

Name	Category	Theorems
`compl` 📖	CompOp	3 math math: `compl_symm`, `mem_compl`, `coe_compl`
`instFintypeElemFinset` 📖	CompOp	—
`instPartialOrderElemFinset` 📖	CompOp	—
`instSetLikeElemFinset` 📖	CompOp	17 math math: `mem_mulActionHom_compl`, `coe_coe`, `stabilizer_coe`, `addAction_stabilizer_coe`, `exists_mem_notMem`, `mem_coe_iff`, `coe_ofFinEmb`, `coe_map`, `mem_ofFinEmb_iff_mem_range`, `mem_compl`, `coe_nonempty_iff`, `mem_ofFinEmbEquiv_iff_mem_range`, `mem_range_ofFinEmbEquiv_symm_iff_mem`, `ncard_eq`, `mem_map_iff_mem_range`, `coe_nontrivial_iff`, `exists_mem_notMem_iff_ne`
`map` 📖	CompOp	3 math math: `coe_map`, `val_map`, `mem_map_iff_mem_range`
`ofFinEmb` 📖	CompOp	5 math math: `val_ofFinEmb`, `ofFinEmb_surjective`, `coe_ofFinEmb`, `mem_ofFinEmb_iff_mem_range`, `ofFinEmbEquiv_apply`
`ofSingleton` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	—	`Nat.card` `Set.Elem` `Finset` `Set.powersetCard` `Nat.choose`	—	`coe_finset` `Nat.card_eq_fintype_card` `Fintype.card_finset_len` `Fintype.card_unique` `Nat.card_eq_zero_of_infinite` `Nat.choose_self` `Nat.choose_zero_succ` `instInfinite`
`card_eq` 📖	mathematical	—	`Finset.card` `Finset` `Set` `Set.instMembership` `Set.powersetCard`	—	`Subtype.prop`
`coe_coe` 📖	mathematical	—	`SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instMembership` `Set.powersetCard` `Set.Elem` `instSetLikeElemFinset`	—	—
`coe_compl` 📖	mathematical	`Fintype.card`	`Finset` `Set` `Set.instMembership` `Set.powersetCard` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `compl` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra`	—	—
`coe_finset` 📖	mathematical	—	`Set.powersetCard` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.powersetCard` `Finset.univ`	—	`Set.ext`
`coe_map` 📖	mathematical	—	`SetLike.coe` `Set.Elem` `Finset` `Set.powersetCard` `instSetLikeElemFinset` `map` `Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Set.ext`
`coe_nonempty_iff` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `Set.Elem` `Finset` `Set.powersetCard` `instSetLikeElemFinset`	—	`coe_coe` `Finset.coe_nonempty` `Finset.one_le_card` `Subtype.prop`
`coe_nontrivial_iff` 📖	mathematical	—	`Set.Nontrivial` `SetLike.coe` `Set.Elem` `Finset` `Set.powersetCard` `instSetLikeElemFinset`	—	`coe_coe` `Finset.nontrivial_coe` `Finset.one_lt_card_iff_nontrivial` `card_eq`
`coe_ofFinEmb` 📖	mathematical	—	`SetLike.coe` `Set.Elem` `Finset` `Set.powersetCard` `instSetLikeElemFinset` `ofFinEmb` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Set.ext`
`compl_symm` 📖	mathematical	`Fintype.card`	`Equiv.symm` `Set.Elem` `Finset` `Set.powersetCard` `compl`	—	—
`eq_empty_iff` 📖	mathematical	—	`Set.powersetCard` `Set` `Finset` `Set.instEmptyCollection` `Nat.card`	—	`Set.ncard_eq_zero` `Set.toFinite` `instFiniteElemFinset` `Nat.card_coe_set_eq` `card` `Nat.choose_eq_zero_iff`
`eq_iff_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Set` `Set.instMembership` `Set.powersetCard`	—	`Finset.subset_iff_eq_of_card_le` `Eq.trans_le` `Subtype.prop` `Eq.ge`
`exist_mem_powersetCard_of_inf` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `Set.powersetCard` `Finset.instMembership`	—	`Infinite.exists_superset_card_eq` `Finset.card_singleton` `mem_iff`
`exists_mem_notMem` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `ENat.card`	`Set.Elem` `Finset` `Set.powersetCard` `SetLike.instMembership` `instSetLikeElemFinset`	—	`ENat.lt_add_one_iff'` `ENat.coe_ne_top` `add_comm` `Set.encard_singleton` `Set.encard_add_encard_compl` `Set.encard_univ` `Set.exists_superset_subset_encard_eq` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Set.finite_of_encard_eq_coe` `mem_iff` `Set.Finite.encard_eq_coe_toFinset_card`
`exists_mem_notMem_iff_ne` 📖	mathematical	—	`Set.Elem` `Finset` `Set.powersetCard` `SetLike.instMembership` `instSetLikeElemFinset`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₂` `Mathlib.Tactic.Push.not_and_eq` `eq_iff_subset`
`instFiniteElemFinset` 📖	mathematical	—	`Finite` `Set.Elem` `Finset` `Set.powersetCard`	—	`coe_finset` `Subtype.finite` `Finite.of_fintype`
`instInfinite` 📖	mathematical	—	`Infinite` `Set.Elem` `Finset` `Set.powersetCard`	—	`not_finite_iff_infinite` `Set.sUnion_eq_univ_iff` `exist_mem_powersetCard_of_inf` `Set.mem_image_of_mem` `Finset.mem_coe` `Finite.false` `Set.finite_univ_iff` `Set.Finite.sUnion` `Set.Finite.image` `Set.sUnion_image` `Set.iUnion_congr_Prop`
`mem_coe_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `Set` `Set.instMembership` `Set.powersetCard` `Set.Elem` `SetLike.instMembership` `instSetLikeElemFinset`	—	—
`mem_compl` 📖	mathematical	`Fintype.card`	`Set.Elem` `Finset` `Set.powersetCard` `SetLike.instMembership` `instSetLikeElemFinset` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `compl`	—	`Finset.mem_compl`
`mem_iff` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `Set.powersetCard` `Finset.card`	—	`eq_1` `Set.mem_setOf_eq`
`mem_map_iff_mem_range` 📖	mathematical	—	`Set.Elem` `Finset` `Set.powersetCard` `SetLike.instMembership` `instSetLikeElemFinset` `map` `Set` `Set.instMembership` `Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `SetLike.coe`	—	—
`mem_ofFinEmb_iff_mem_range` 📖	mathematical	—	`Set.Elem` `Finset` `Set.powersetCard` `SetLike.instMembership` `instSetLikeElemFinset` `ofFinEmb` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	—
`ncard_eq` 📖	mathematical	—	`Set.ncard` `SetLike.coe` `Set.Elem` `Finset` `Set.powersetCard` `instSetLikeElemFinset`	—	`coe_coe` `Set.ncard_coe_finset` `Subtype.prop`
`nontrivial` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `ENat.card`	`Nontrivial` `Set.Elem` `Finset` `Set.powersetCard`	—	`Set.nontrivial_coe_sort` `Set.one_lt_ncard_iff_nontrivial` `instFiniteElemFinset` `Finite.of_fintype` `Nat.card_coe_set_eq` `card` `lt_self_iff_false` `lt_trans` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENat.card_eq_coe_natCard` `Nat.choose_eq_zero_iff` `Nat.card_eq_fintype_card` `Nat.choose_eq_one_iff` `NeZero.of_pos` `Infinite.instNontrivial` `instInfinite`
`nontrivial'` 📖	mathematical	`Nat.card`	`Nontrivial` `Set.Elem` `Finset` `Set.powersetCard`	—	`Nat.finite_of_card_ne_zero` `ne_zero_of_lt` `nontrivial` `ENat.card_eq_coe_natCard` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `Set.Elem` `Finset` `Set.powersetCard` `Nat.card`	—	`Finite.one_lt_card_iff_nontrivial` `instFiniteElemFinset` `card` `Nat.choose_eq_zero_iff` `Nat.choose_eq_one_iff`
`ofFinEmb_surjective` 📖	mathematical	—	`Function.Embedding` `Set.Elem` `Finset` `Set.powersetCard` `ofFinEmb`	—	`Function.Embedding.exists_of_card_eq_finset` `Fintype.card_fin`
`val_map` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `Set.powersetCard` `map` `Finset.map`	—	—
`val_ofFinEmb` 📖	mathematical	—	`Finset` `Set` `Set.instMembership` `Set.powersetCard` `ofFinEmb` `Finset.map` `Finset.univ` `Fin.fintype`	—	`coe_ofFinEmb` `Finset.coe_map` `Finset.coe_univ` `Set.image_univ`

---

← Back to Index