Theorems · Inductive type · order theory

SetLike

Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)

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

Cited by

1,084 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms