Theorems · Theorem · logic and foundations

Part.mem_assert

∀ {α : Type u_1} {p : Prop} {f : p → Part α} {a : α} (h : p), a ∈ f h → a ∈ Part.assert p f

Defined in

Mathlib.Data.Part

Cited by

2 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms