Mathlib Map

Structures · Lean core

Membership

The typeclass behind the notation a ∈ s : Prop where a : α, s : γ. Because α is an outParam, the "container type" γ determines the type of the elements of the container.

Defined in
Init.Prelude
Shape
2 explicit arguments · adds mem
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances17

  • Int
  • Nat
  • Real
  • Associates
  • Projectivization
  • Class
  • PSet
  • PFun
  • Configuration.Dual
  • BoxIntegral.Box
  • Std.Http.Header.Name
  • Lists
  • OpenPartialHomeomorph
  • Std.Sat.CNF.Clause
  • Prod
  • List
  • Set

How is a type an instance?

Loading the hierarchy index…

Assumed by42

Ancestors0

No ancestors.