Skip to content

Commit

Permalink
doc(data/set/basic): add pointer to iff versions (#17300)
Browse files Browse the repository at this point in the history
  • Loading branch information
kmill committed Nov 5, 2022
1 parent 8b88983 commit 58b7f91
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/data/set/basic.lean
Expand Up @@ -298,6 +298,7 @@ lemma nonempty_of_mem {x} (h : x ∈ s) : s.nonempty := ⟨x, h⟩
theorem nonempty.not_subset_empty : s.nonempty → ¬(s ⊆ ∅)
| ⟨x, hx⟩ hs := hs hx

/-- See also `set.ne_empty_iff_nonempty` and `set.not_nonempty_iff_eq_empty`. -/
theorem nonempty.ne_empty : ∀ {s : set α}, s.nonempty → s ≠ ∅
| _ ⟨x, hx⟩ rfl := hx

Expand Down

0 comments on commit 58b7f91

Please sign in to comment.