Merge branch 'master' into angle_incenter_unoriented

Author: jsm28

Mathlib/Topology/Algebra/MulAction.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.AddTorsor.Defs
 public import Mathlib.GroupTheory.GroupAction.SubMulAction
+public import Mathlib.Order.Filter.Pointwise
 public import Mathlib.Topology.Algebra.Constructions
 public import Mathlib.Topology.Algebra.ConstMulAction
 public import Mathlib.Topology.Connected.Basic
@@ -230,6 +231,28 @@ lemma stabilizer_isOpen [DiscreteTopology X] (x : X) : IsOpen (MulAction.stabili
 
 end Group
 
+section GroupWithZero
+
+variable {G₀ X : Type*} [GroupWithZero G₀] [Zero X] [MulActionWithZero G₀ X]
+  [TopologicalSpace G₀] [(𝓝[≠] (0 : G₀)).NeBot] [TopologicalSpace X] [ContinuousSMul G₀ X]
+
+theorem Set.univ_smul_nhds_zero {s : Set X} (hs : s ∈ 𝓝 0) : (univ : Set G₀) • s = Set.univ := by
+  refine Set.eq_univ_of_forall fun x ↦ ?_
+  have : Tendsto (· • x) (𝓝 (0 : G₀)) (𝓝 0) :=
+    zero_smul G₀ x ▸ tendsto_id.smul tendsto_const_nhds
+  rcases Filter.nonempty_of_mem (inter_mem_nhdsWithin {0}ᶜ <| mem_map.1 <| this hs)
+    with ⟨c, hc₀, hc⟩
+  refine ⟨c⁻¹, trivial, c • x, hc, ?_⟩
+  simp_all
+
+@[simp]
+theorem Filter.top_smul_nhds_zero : (⊤ : Filter G₀) • 𝓝 (0 : X) = ⊤ := by
+  rw [(hasBasis_top.smul (basis_sets _)).eq_top_iff]
+  rintro ⟨_, s⟩ ⟨-, hs⟩
+  exact Set.univ_smul_nhds_zero hs
+
+end GroupWithZero
+
 @[to_additive]
 instance Prod.continuousSMul [SMul M X] [SMul M Y] [ContinuousSMul M X] [ContinuousSMul M Y] :
     ContinuousSMul M (X × Y) :=

Mathlib/Topology/MetricSpace/Congruence.lean

@@ -6,6 +6,7 @@ Authors: Jovan Gerbscheid, Newell Jensen
 module
 
 public import Mathlib.Topology.MetricSpace.Pseudo.Defs
+public import Mathlib.Topology.MetricSpace.Isometry
 
 /-!
 # Congruences
@@ -96,6 +97,20 @@ lemma index_map (h : v₁ ≅ v₂) (f : ι' → ι) : (v₁ ∘ f) ≅ (v₂ 
   simpa [(EquivLike.toEquiv f).right_inv i₁, (EquivLike.toEquiv f).right_inv i₂]
     using edist_eq h ((EquivLike.toEquiv f).symm i₁) ((EquivLike.toEquiv f).symm i₂)
 
+lemma comp_left {f : P₁ → P₃} (hf : Isometry f) (h : v₁ ≅ v₂) : f ∘ v₁ ≅ v₂ :=
+  .trans (fun _ _ ↦ hf _ _) h
+
+lemma comp_right {f : P₂ → P₃} (hf : Isometry f) (h : v₁ ≅ v₂) : v₁ ≅ f ∘ v₂ :=
+  .trans h (.symm <| fun _ _ ↦ hf _ _)
+
+@[simp]
+lemma comp_left_iff {f : P₁ → P₃} (hf : Isometry f) : f ∘ v₁ ≅ v₂ ↔ v₁ ≅ v₂ :=
+  ⟨.trans <| .comp_right hf (.refl _), .comp_left hf⟩
+
+@[simp]
+lemma comp_right_iff {f : P₂ → P₃} (hf : Isometry f) : v₁ ≅ f ∘ v₂ ↔ v₁ ≅ v₂ := by
+  rw [congruent_comm, comp_left_iff hf, congruent_comm]
+
 end Congruent
 
 end PseudoEMetricSpace

Mathlib/Topology/MetricSpace/Similarity.lean

@@ -6,6 +6,7 @@ Authors: Jovan Gerbscheid, Newell Jensen
 module
 
 public import Mathlib.Topology.MetricSpace.Congruence
+public import Mathlib.Topology.MetricSpace.Dilation
 public import Mathlib.Tactic.FinCases
 
 /-!
@@ -113,6 +114,53 @@ lemma index_equiv (f : ι' ≃ ι) (v₁ : ι → P₁) (v₂ : ι → P₂) :
   refine ⟨r, hr, fun i₁ i₂ => ?_⟩
   simpa [f.right_inv i₁, f.right_inv i₂] using h (f.symm i₁) (f.symm i₂)
 
+/-! Similarity is preserved under dilations. -/
+
+section Dilation
+variable {F}
+
+lemma comp_left [FunLike F P₁ P₃] [DilationClass F P₁ P₃] (f : F) (h : v₁ ∼ v₂) :
+    f ∘ v₁ ∼ v₂ :=
+  .trans ⟨Dilation.ratio f, Dilation.ratio_ne_zero f, fun _ _ => Dilation.edist_eq f _ _⟩ h
+
+lemma comp_right [FunLike F P₂ P₃] [DilationClass F P₂ P₃] (f : F) (h : v₁ ∼ v₂) : v₁ ∼ f ∘ v₂ :=
+  .symm (h.symm.comp_left f)
+
+@[simp]
+lemma comp_left_iff [FunLike F P₁ P₃] [DilationClass F P₁ P₃] (f : F) : f ∘ v₁ ∼ v₂ ↔ v₁ ∼ v₂ :=
+  ⟨.trans <| .comp_right f (.refl _), .comp_left f⟩
+
+@[simp]
+lemma comp_right_iff [FunLike F P₂ P₃] [DilationClass F P₂ P₃] (f : F) : v₁ ∼ f ∘ v₂ ↔ v₁ ∼ v₂ := by
+  rw [similar_comm, comp_left_iff, similar_comm]
+
+end Dilation
+
+/-! Similarity is preserved under isometries.
+
+While these are trivial consequences of the dilation results, they avoid ending up with a
+`toDilation` in the expression, and so are easier to apply to plain functions.
+If `Dilation` were a predicate like `Isometry` then these would not be needed.
+-/
+
+section Isometry
+
+lemma comp_isometry_left {f : P₁ → P₃} (hf : Isometry f) (h : v₁ ∼ v₂) : f ∘ v₁ ∼ v₂ :=
+  comp_left hf.toDilation h
+
+lemma comp_isometry_right {f : P₂ → P₃} (hf : Isometry f) (h : v₁ ∼ v₂) : v₁ ∼ f ∘ v₂ :=
+  comp_right hf.toDilation h
+
+@[simp]
+lemma comp_isometry_left_iff {f : P₁ → P₃} (hf : Isometry f) : f ∘ v₁ ∼ v₂ ↔ v₁ ∼ v₂ :=
+  comp_left_iff hf.toDilation
+
+@[simp]
+lemma comp_isometry_right_iff {f : P₂ → P₃} (hf : Isometry f) : v₁ ∼ f ∘ v₂ ↔ v₁ ∼ v₂ :=
+  comp_right_iff hf.toDilation
+
+end Isometry
+
 section Triangle
 
 variable {a b c : P₁} {a' b' c' : P₂}