Coercing sets to types.

This file defines Set.Elem s as the type of all elements of the set s. More advanced theorems about these definitions are located in other files in Mathlib/Data/Set.

Main definitions

• Set.Elem: coercion of a set to a type; it is reducibly equal to {x // x ∈ s};

@[reducible]

def Set.Elem {α : Type u} (s : Set α) : Type u

Given the set s, Elem s is the Type of element of s.

It is currently an abbreviation so that instance coming from Subtype are available. If you're interested in making it a def, as it probably should be, you'll then need to create additional instances (and possibly prove lemmas about them). See e.g. Mathlib.Data.Set.Order.

Equations

• ↑s = { x : α // x ∈ s }

Instances For

• Finite.Set.finite_diff
• Finite.Set.finite_image
• Finite.Set.finite_image2
• Finite.Set.finite_insert
• Finite.Set.finite_inter_of_left
• Finite.Set.finite_inter_of_right
• Finite.Set.finite_prod
• Finite.Set.finite_range
• Finite.Set.finite_replacement
• Finite.Set.finite_sep
• Finite.Set.finite_union
• Finset.instNonemptyElemToSetInsert
• FinsetCoe.fintype
• IsAtomic.Set.Iic.isAtomic
• IsCoatomic.Set.Ici.isCoatomic
• IsModularLattice.complementedLattice_Ici
• IsModularLattice.complementedLattice_Iic
• IsModularLattice.isModularLattice_Ici
• IsModularLattice.isModularLattice_Iic
• Set.Icc.completeLattice
• Set.Icc.instBoundedOrderElem
• Set.Icc.instOrderBotElem
• Set.Icc.instOrderTopElem
• Set.Icc.lattice
• Set.Icc.semilatticeInf
• Set.Icc.semilatticeSup
• Set.Ici.boundedOrder
• Set.Ici.distribLattice
• Set.Ici.lattice
• Set.Ici.orderBot
• Set.Ici.orderTop
• Set.Ici.semilatticeInf
• Set.Ici.semilatticeSup
• Set.Ico.semilatticeInf
• Set.Iic.instBoundedOrderElemOfOrderBot
• Set.Iic.instCompleteLattice
• Set.Iic.instLatticeElem
• Set.Iic.orderBot
• Set.Iic.orderTop
• Set.Iic.semilatticeInf
• Set.Iic.semilatticeSup
• Set.Iio.semilatticeInf
• Set.Ioc.semilatticeSup
• Set.Ioi.semilatticeSup
• Set.OrdConnected.predOrder
• Set.OrdConnected.succOrder
• Set.fintypeDiff
• Set.fintypeDiffLeft
• Set.fintypeEmpty
• Set.fintypeImage
• Set.fintypeImage2
• Set.fintypeInsert
• Set.fintypeInsert'
• Set.fintypeInter
• Set.fintypeInterOfLeft
• Set.fintypeInterOfRight
• Set.fintypeLENat
• Set.fintypeLTNat
• Set.fintypeMap
• Set.fintypeMemFinset
• Set.fintypeOffDiag
• Set.fintypeProd
• Set.fintypeRange
• Set.fintypeSep
• Set.fintypeSingleton
• Set.fintypeTop
• Set.fintypeUnion
• Set.fintypeUniv
• Set.instDenselyOrdered
• Set.instIccUnique
• Set.instIsEmptyElemEmptyCollection
• Set.instNoMaxOrderElemIci
• Set.instNoMaxOrderElemIoi
• Set.instNoMinOrderElemIic
• Set.instNoMinOrderElemIio
• Set.instNonemptyElemImage
• Set.instNonemptyElemInsert
• Set.instNonemptyRange
• Set.instNonemptyTop
• Set.nonempty_Ici_subtype
• Set.nonempty_Iic_subtype
• Set.nonempty_Iio_subtype
• Set.nonempty_Ioi_subtype
• Set.subsingleton_coe_of_subsingleton
• Set.uniqueSingleton
• Set.univ.nonempty
• instCoeTCElem
• instCompleteLinearOrderElemIccOfFactLe
• instIsStronglyAtomicElemOfOrdConnected
• instIsStronglyCoatomicElemOfOrdConnected
• instNoMaxOrderElemIco
• instNoMaxOrderElemIio
• instNoMaxOrderElemIoo
• instNoMinOrderElemIoc
• instNoMinOrderElemIoi
• instNoMinOrderElemIoo
• ordConnectedSubsetConditionallyCompleteLinearOrder

instance Set.instCoeSortType {α : Type u} : CoeSort (Set α) (Type u)

Coercion from a set to the corresponding subtype.

Equations

• Set.instCoeSortType = { coe := Set.Elem }