Mathlib Map

Structures · Data types

SetLike

A class to indicate that there is a canonical injection between A and Set B. This has the effect of giving terms of A elements of type B (through a Membership instance) and a compatible coercion to Type* as a subtype. Note: if SetLike.coe is a projection, implementers should create a simp lemma such as `` @[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl ` to normalize terms. If you declare an unbundled subclass of SetLike, for example: ` class MulMemClass (S : Type*) (M : Type*) [Mul M] [SetLike S M] where ... ` Then you should *not* repeat the outParam declaration so SetLike will supply the value instead. This ensures your subclass will not have issues with synthesis of the [Mul M] parameter starting before the value of M` is known.

Defined in
Mathlib.Data.SetLike.Basic
Shape
2 explicit arguments · adds coe, coe_injective
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Forgetful instances

Every SetLike is also a

Concrete types that are instances98

  • NonemptyInterval
  • Interval
  • TopologicalSpace.NonemptyCompacts
  • FractionalIdeal
  • UpperSet
  • LowerSet
  • LieSubalgebra
  • LieSubmodule
  • TopologicalSpace.Opens
  • TopologicalSpace.Compacts
  • AddSubgroup
  • Sym2
  • AddSubmonoid
  • NonUnitalSubalgebra
  • NonUnitalStarSubalgebra
  • Sublattice
  • BooleanSubalgebra
  • SimpleGraph.ConnectedComponent
  • TopologicalSpace.Closeds
  • SubMulAction
  • TopologicalSpace.OpenNhdsOf
  • ConvexBody
  • Partition
  • ConvexCone
  • StarSubalgebra
  • Flag
  • TopologicalSpace.Clopens
  • ClosedSubmodule
  • TwoSidedIdeal
  • HomogeneousIdeal
  • AffineSubspace
  • NonUnitalSubring
  • Sublocale
  • NonUnitalSubsemiring
  • SubAddAction
  • SaturatedAddSubmonoid
  • AddSubsemigroup
  • SaturatedSubmonoid
  • Order.Ideal
  • TopologicalSpace.CompactOpens
  • ZFSet
  • StructureGroupoid
  • CategoryTheory.Subgroupoid
  • FirstOrder.Language.Substructure
  • DividedPowers.SubDPIdeal
  • AbstractSimplicialComplex
  • PreAbstractSimplicialComplex
  • Projectivization.Subspace
  • FirstOrder.Language.DefinableSet
  • OpenSubgroup
  • OpenAddSubgroup
  • OpenNormalAddSubgroup
  • OpenNormalSubgroup
  • FiniteIndexNormalSubgroup
  • FiniteIndexNormalAddSubgroup
  • Sylow
  • ValuationSubring
  • FirstOrder.Language.Theory.CompleteType
  • ClosedSubgroup
  • ClosedAddSubgroup
  • ClopenUpperSet
  • LieRinehartSubalgebra
  • Subrepresentation
  • YoungDiagram
  • VonNeumannAlgebra
  • RingCone
  • FirstOrder.Language.ElementarySubstructure
  • SimpleGraph.ComponentCompl
  • StarSubsemiring
  • RingPreordering
  • MeasureTheory.MeasuredSets
  • HomogeneousSubsemiring
  • TopologicalSpace.PositiveCompacts
  • Order.PFilter
  • AddGroupCone
  • GroupCone
  • HomogeneousSubmodule
  • ProperCone
  • CompleteSublattice
  • RelUpperSet
  • Topology.RelCWComplex.Subcomplex
  • NonemptyChain
  • TopologicalSpace.IrreducibleCloseds
  • NonUnitalStarSubsemiring
  • RelLowerSet
  • SubRootedTree
  • Subtype
  • Set.Elem
  • Submodule
  • Finset
  • Subgroup
  • IntermediateField
  • Subalgebra
  • Subfield
  • Submonoid
  • Subring
  • Subsemiring
  • Subsemigroup

How is a type an instance?

Loading the hierarchy index…

Assumed by1,542

Ancestors3