feat(data/set/basic): Add natural missing lemmas to `set.subsingleton…

…` and slightly refactor (#15886)

- `subsingleton.image` is moved and documentation is added so that it is near related lemmas.
- `subsingleton_of_preimage` is added to go with `subsingleton.preimage`, `subsingleton_of_image`., and `subsingleton.image`.
- We add `subsingleton_anti` analogously to `nontrivial_mono`.
- Some small style tweaks are made.
- `subsingleton.mono` is renamed to `subsingleton.anti`.





Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>

src/data/set/basic.lean

@@ -1683,18 +1683,14 @@ end image
 
 /-! ### Subsingleton -/
 
-/-- A set `s` is a `subsingleton`, if it has at most one element. -/
+/-- A set `s` is a `subsingleton` if it has at most one element. -/
 protected def subsingleton (s : set α) : Prop :=
 ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), x = y
 
-lemma subsingleton.mono (ht : t.subsingleton) (hst : s ⊆ t) : s.subsingleton :=
+lemma subsingleton.anti (ht : t.subsingleton) (hst : s ⊆ t) : s.subsingleton :=
 λ x hx y hy, ht (hst hx) (hst hy)
 
-lemma subsingleton.image (hs : s.subsingleton) (f : α → β) : (f '' s).subsingleton :=
-λ _ ⟨x, hx, Hx⟩ _ ⟨y, hy, Hy⟩, Hx ▸ Hy ▸ congr_arg f (hs hx hy)
-
-lemma subsingleton.eq_singleton_of_mem (hs : s.subsingleton) {x:α} (hx : x ∈ s) :
-  s = {x} :=
+lemma subsingleton.eq_singleton_of_mem (hs : s.subsingleton) {x:α} (hx : x ∈ s) : s = {x} :=
 ext $ λ y, ⟨λ hy, (hs hx hy) ▸ mem_singleton _, λ hy, (eq_of_mem_singleton hy).symm ▸ hx⟩
 
 @[simp] lemma subsingleton_empty : (∅ : set α).subsingleton := λ x, false.elim
@@ -1703,7 +1699,7 @@ ext $ λ y, ⟨λ hy, (hs hx hy) ▸ mem_singleton _, λ hy, (eq_of_mem_singleto
 λ x hx y hy, (eq_of_mem_singleton hx).symm ▸ (eq_of_mem_singleton hy).symm ▸ rfl
 
 lemma subsingleton_of_subset_singleton (h : s ⊆ {a}) : s.subsingleton :=
-subsingleton_singleton.mono h
+subsingleton_singleton.anti h
 
 lemma subsingleton_of_forall_eq (a : α) (h : ∀ b ∈ s, b = a) : s.subsingleton :=
 λ b hb c hc, (h _ hb).trans (h _ hc).symm
@@ -1729,7 +1725,7 @@ lemma subsingleton_of_univ_subsingleton (h : (univ : set α).subsingleton) : sub
 ⟨subsingleton_of_univ_subsingleton, λ h, @subsingleton_univ _ h⟩
 
 lemma subsingleton_of_subsingleton [subsingleton α] {s : set α} : set.subsingleton s :=
-subsingleton.mono subsingleton_univ (subset_univ s)
+subsingleton_univ.anti (subset_univ s)
 
 lemma subsingleton_is_top (α : Type*) [partial_order α] : set.subsingleton {x : α | is_top x} :=
 λ x hx y hy, hx.is_max.eq_of_le (hy x)
@@ -1746,8 +1742,7 @@ begin
   { exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty },
 end
 
-/-- `s`, coerced to a type, is a subsingleton type if and only if `s`
-is a subsingleton set. -/
+/-- `s`, coerced to a type, is a subsingleton type if and only if `s` is a subsingleton set. -/
 @[simp, norm_cast] lemma subsingleton_coe (s : set α) : subsingleton s ↔ s.subsingleton :=
 begin
   split,
@@ -1761,16 +1756,24 @@ For the corresponding result for `subtype`, see `subtype.subsingleton`. -/
 instance subsingleton_coe_of_subsingleton [subsingleton α] {s : set α} : subsingleton s :=
 by { rw [s.subsingleton_coe], exact subsingleton_of_subsingleton }
 
+/-- The image of a subsingleton is a subsingleton. -/
+lemma subsingleton.image (hs : s.subsingleton) (f : α → β) : (f '' s).subsingleton :=
+λ _ ⟨x, hx, Hx⟩ _ ⟨y, hy, Hy⟩, Hx ▸ Hy ▸ congr_arg f (hs hx hy)
+
 /-- The preimage of a subsingleton under an injective map is a subsingleton. -/
 theorem subsingleton.preimage {s : set β} (hs : s.subsingleton) {f : α → β}
-  (hf : function.injective f) :
-  (f ⁻¹' s).subsingleton :=
-λ a ha b hb, hf $ hs ha hb
+  (hf : function.injective f) : (f ⁻¹' s).subsingleton := λ a ha b hb, hf $ hs ha hb
 
-/-- `s` is a subsingleton, if its image of an injective function is. -/
+/-- If the image of a set under an injective map is a subsingleton, the set is a subsingleton. -/
 theorem subsingleton_of_image {α β : Type*} {f : α → β} (hf : function.injective f)
   (s : set α) (hs : (f '' s).subsingleton) : s.subsingleton :=
-(hs.preimage hf).mono $ subset_preimage_image _ _
+(hs.preimage hf).anti $ subset_preimage_image _ _
+
+/-- If the preimage of a set under an surjective map is a subsingleton,
+the set is a subsingleton. -/
+theorem subsingleton_of_preimage {α β : Type*} {f : α → β} (hf : function.surjective f)
+  (s : set β) (hs : (f ⁻¹' s).subsingleton) : s.subsingleton :=
+λ fx hx fy hy, by { rcases ⟨hf fx, hf fy⟩ with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩, exact congr_arg f (hs hx hy) }
 
 /-! ### Nontrivial -/
 

src/data/set/pointwise.lean

@@ -1236,7 +1236,7 @@ lemma zero_smul_set_subset (s : set β) : (0 : α) • s ⊆ 0 :=
 image_subset_iff.2 $ λ x _, zero_smul α x
 
 lemma subsingleton_zero_smul_set (s : set β) : ((0 : α) • s).subsingleton :=
-subsingleton_singleton.mono $ zero_smul_set_subset s
+subsingleton_singleton.anti $ zero_smul_set_subset s
 
 lemma zero_mem_smul_set {t : set β} {a : α} (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
 ⟨0, h, smul_zero' _ _⟩

src/measure_theory/measure/hausdorff.lean

@@ -883,7 +883,7 @@ begin
     { simp only [hs, measure_empty, zero_le], },
     have : f ⁻¹' s = {x},
     { haveI : subsingleton X := hf.subsingleton,
-      have : (f ⁻¹' s).subsingleton, from subsingleton_univ.mono (subset_univ _),
+      have : (f ⁻¹' s).subsingleton, from subsingleton_univ.anti (subset_univ _),
       exact (subsingleton_iff_singleton hx).1 this },
     rw this,
     rcases eq_or_lt_of_le hd with rfl|h'd,

src/topology/connected.lean

@@ -1246,7 +1246,7 @@ theorem is_totally_disconnected_empty : is_totally_disconnected (∅ : set α) :
 λ _ ht _ _ x_in _ _, (ht x_in).elim
 
 theorem is_totally_disconnected_singleton {x} : is_totally_disconnected ({x} : set α) :=
-λ _ ht _, subsingleton.mono subsingleton_singleton ht
+λ _ ht _, subsingleton_singleton.anti ht
 
 /-- A space is totally disconnected if all of its connected components are singletons. -/
 class totally_disconnected_space (α : Type u) [topological_space α] : Prop :=
@@ -1322,7 +1322,7 @@ begin
   intros s s_sub hs,
   rcases eq_empty_or_nonempty s with rfl | ⟨x, x_in⟩,
   { exact subsingleton_empty },
-  { exact (h x).mono (hs.subset_connected_component x_in) }
+  { exact (h x).anti (hs.subset_connected_component x_in) }
 end
 
 /-- A space is totally disconnected iff its connected components are singletons. -/

src/topology/metric_space/basic.lean

@@ -2564,7 +2564,7 @@ begin
 end
 
 lemma subsingleton_sphere (x : γ) {r : ℝ} (hr : r ≤ 0) : (sphere x r).subsingleton :=
-(subsingleton_closed_ball x hr).mono sphere_subset_closed_ball
+(subsingleton_closed_ball x hr).anti sphere_subset_closed_ball
 
 /-- A map between metric spaces is a uniform embedding if and only if the distance between `f x`
 and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/

src/topology/separation.lean

@@ -516,7 +516,7 @@ hs.induction_on (by simp) $ λ x, by simp
 
 @[simp] lemma subsingleton_closure [t1_space α] {s : set α} :
   (closure s).subsingleton ↔ s.subsingleton :=
-⟨λ h, h.mono subset_closure, λ h, h.closure⟩
+⟨λ h, h.anti subset_closure, λ h, h.closure⟩
 
 lemma is_closed_map_const {α β} [topological_space α] [topological_space β] [t1_space β] {y : β} :
   is_closed_map (function.const α y) :=