Skip to content

Commit

Permalink
Fix: fix case in a dot notation lemma (#1886)
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud committed Jan 27, 2023
1 parent 8b47448 commit cd8220b
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Data/Set/Basic.lean
Expand Up @@ -260,9 +260,9 @@ theorem mem_setOf {a : α} {p : α → Prop} : a ∈ { x | p x } ↔ p a :=
/-- If `h : a ∈ {x | p x}` then `h.out : p x`. These are definitionally equal, but this can
nevertheless be useful for various reasons, e.g. to apply further projection notation or in an
argument to `simp`. -/
theorem _root_.Membership.Mem.out {p : α → Prop} {a : α} (h : a ∈ { x | p x }) : p a :=
theorem _root_.Membership.mem.out {p : α → Prop} {a : α} (h : a ∈ { x | p x }) : p a :=
h
#align has_mem.mem.out Membership.Mem.out
#align has_mem.mem.out Membership.mem.out

theorem nmem_setOf_iff {a : α} {p : α → Prop} : a ∉ { x | p x } ↔ ¬p a :=
Iff.rfl
Expand Down

0 comments on commit cd8220b

Please sign in to comment.