Theorems · Definition · logic and foundations

Part.assert

{α : Type u_1} → (p : Prop) → (p → Part α) → Part α

assert p f is a bind-like operation which appends an additional condition p to the domain and uses f to produce the value.

Defined in

Mathlib.Data.Part

Cited by

10 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms