Theorems · Theorem · logic and foundations

Part.mem_assert_iff

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

Defined in

Mathlib.Data.Part

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms