Sakai 1.7.5

LeanOA.lean

@@ -10,14 +10,17 @@ import LeanOA.KreinSmulian
 import LeanOA.Lp.Holder
 import LeanOA.Lp.lpSpace
 import LeanOA.Masa
+import LeanOA.Mathlib.Algebra.LinearAlgebra.Span.Defs
 import LeanOA.Mathlib.Algebra.Order.Module.PositiveLinearMap
 import LeanOA.Mathlib.Algebra.Order.Star.Basic
 import LeanOA.Mathlib.Algebra.Order.Star.Conjugate
 import LeanOA.Mathlib.Algebra.Star.StarAlgHom
+import LeanOA.Mathlib.Algebra.Star.Unitary
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ApproximateUnit
 import LeanOA.Mathlib.Analysis.CStarAlgebra.Basic
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Transfer
 import LeanOA.Mathlib.Analysis.CStarAlgebra.GelfandDuality
 import LeanOA.Mathlib.Analysis.CStarAlgebra.Module.Defs
@@ -44,6 +47,7 @@ import LeanOA.Ultraweak.Bornology
 import LeanOA.Ultraweak.ContinuousFunctionalCalculus
 import LeanOA.Ultraweak.ContinuousStar
 import LeanOA.Ultraweak.LUB
+import LeanOA.Ultraweak.Masa
 import LeanOA.Ultraweak.OrderClosed
 import LeanOA.Ultraweak.SeparatingDual
 import LeanOA.Ultraweak.Uniformity

LeanOA/ExtremallyDisconnected.lean

@@ -50,8 +50,8 @@ theorem ExtremallyDisconnected.ofConditionallyCompletePartialOrderSupContinuousM
       simp [h1 (by simpa using hx)]
     simpa [← isClosed_compl_iff, key] using isClosed_singleton.preimage (map_continuous f)
   intro s hs hsn hb
-  obtain ⟨g', hg⟩ := h _ (hs.mono_comp (monotone_realToRCLike K 𝕜)) (hsn.image _)
-    ((monotone_realToRCLike K 𝕜).map_bddAbove hb)
+  obtain ⟨g', hg⟩ := h _ (hs.mono_comp (realToRCLike_monotone K 𝕜)) (hsn.image _)
+    ((realToRCLike_monotone K 𝕜).map_bddAbove hb)
   rw [← isSelfAdjoint_realToRCLike.of_ge (hg.1 ⟨_, hsn.some_mem, rfl⟩)
     |>.realToRCLike_rclikeToReal] at hg
   exact ⟨_, hg.of_image <| by simp [le_def]⟩

LeanOA/Masa.lean

@@ -30,12 +30,11 @@ instance Algebra.instIsMulCommutativeAdjoin {S R A : Type*} [CommSemiring R]
   let := adjoinCommSemiringOfComm R hs.setLike_mul_comm
   ⟨⟨mul_comm⟩⟩
 
-instance NonUnitalAlgebra.instIsMulCommutativeAdjoin {S R A : Type*} [CommSemiring R]
-    [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
-    [SetLike S A] [MulMemClass S A] (s : S) [hs : IsMulCommutative s] :
-    IsMulCommutative (adjoin R (s : Set A)) :=
-  let := adjoinNonUnitalCommSemiringOfComm R hs.setLike_mul_comm
-  ⟨⟨mul_comm⟩⟩
+lemma setLike_mul_comm_star {S A : Type*}
+    [Semigroup A] [StarMul A] [SetLike S A] [MulMemClass S A] [StarMemClass S A]
+    {s : S} [hs : IsMulCommutative s] ⦃a b : A⦄ (ha : a ∈ s) (hb : b ∈ s) :
+    a * star b = star b * a :=
+  IsMulCommutative.setLike_mul_comm inferInstance a ha (star b) (star_mem hb)
 
 instance NonUnitalStarAlgebra.instIsMulCommutativeAdjoin {S R A : Type*} [CommSemiring R]
     [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
@@ -411,6 +410,42 @@ theorem NonUnitalStarSubalgebra.exists_le_isMasa (B : NonUnitalStarSubalgebra R
   have hC' := C.prop.1
   exact ⟨fun S hS hCS ↦ @hC ⟨S, hS, C.prop.2.trans hCS⟩ hCS⟩
 
+/-- If all elements of `s : Set A` commute pairwise and with elements of `star s`, then `adjoin R s`
+is commutative. -/
+theorem NonUnitalStarAlgebra.isMulCommutative_adjoin (R : Type*) {A : Type*} [CommSemiring R]
+    [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A]
+    [SMulCommClass R A A] [StarModule R A] {s : Set A} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x)
+    (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) :
+    IsMulCommutative (adjoin R s) := by
+  have := adjoin_le_centralizer_centralizer R s
+  refine .of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_
+  have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
+    Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha)
+      (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha
+  apply this at h₁
+  apply this at h₂
+  rw [← SetLike.mem_coe, NonUnitalStarSubalgebra.coe_centralizer_centralizer] at h₁ h₂
+  exact Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂
+
+attribute [grind →] Commute.eq star_comm_self
+
+open NonUnitalStarAlgebra in
+/-- A normal element which commutes with every element of a masa is itself in the masa. -/
+theorem NonUnitalStarSubalgebra.IsMasa.mem_of_commute (B : NonUnitalStarSubalgebra R A)
+    [hB : IsMasa B] {x : A} [IsStarNormal x] (hx : ∀ y ∈ B, Commute x y) : x ∈ B := by
+  let S : NonUnitalStarSubalgebra R A := adjoin R ({x} ∪ B)
+  suffices IsMulCommutative S by
+    replace hx : x ∈ S := subset_adjoin R _ <| by simp
+    exact hB.maximal S (fun y hy ↦ subset_adjoin R _ (by aesop)) hx
+  have hx₀ : star x * x = x * star x := star_comm_self' x
+  have hx₁ : ∀ y : B, Commute x (star y) := by
+    rw [star_involutive.surjective.forall]; simpa using hx
+  have hx₂ : ∀ y : B, Commute (star x) y := by simpa [commute_star_comm] using hx₁
+  have hB₀ : ∀ a ∈ B, ∀ b ∈ B, a * b = b * a := IsMulCommutative.setLike_mul_comm inferInstance
+  have hB₁ := setLike_mul_comm_star (s := B)
+  refine isMulCommutative_adjoin R ?_ ?_
+  all_goals simp [commute_iff_eq] at *; grind
+
 end NonUnitalStarSubalgebra
 
 section TopologicalAlgebra
@@ -473,6 +508,12 @@ lemma StarSubalgebra.exists_le_isMasa (B : StarSubalgebra R A) [hB : IsMulCommut
   have ⟨C, hC⟩ := B.toNonUnitalStarSubalgebra.exists_le_isMasa
   ⟨C.toStarSubalgebra hC.2.one_mem, hC⟩
 
+/-- A normal element which commutes with every element of a masa is itself in the masa. -/
+theorem StarSubalgebra.IsMasa.mem_of_commute (B : StarSubalgebra R A)
+    [hB : IsMasa B] {x : A} [IsStarNormal x] (hx : ∀ y ∈ B, Commute x y) : x ∈ B := by
+  rw [← mem_toNonUnitalStarSubalgebra]
+  exact NonUnitalStarSubalgebra.IsMasa.mem_of_commute B.toNonUnitalStarSubalgebra hx
+
 /-- A masa in a topological star algebra is closed. -/
 instance StarSubalgebra.IsMasa.isClosed [TopologicalSpace A] [IsTopologicalSemiring A]
     [ContinuousStar A] [T2Space A] (B : StarSubalgebra R A)

LeanOA/Mathlib/Algebra/LinearAlgebra/Span/Defs.lean

@@ -0,0 +1,28 @@
+module
+
+public import Mathlib.LinearAlgebra.Span.Defs
+
+public section CommuteSpan
+
+variable {R M : Type*} [CommSemiring R] [NonUnitalNonAssocSemiring M] [Module R M]
+  [IsScalarTower R M M] [SMulCommClass R M M]
+
+/-- If every element of a set `s` commutes with `x`, then every element of `Submodule.span R s`
+commutes with `x`. -/
+theorem Commute.span_left {s : Set M} {x : M} (h : ∀ y ∈ s, Commute y x) :
+    ∀ y ∈ Submodule.span R s, Commute y x := by
+  intro y hy
+  induction hy using Submodule.span_induction with
+  | mem _ _ => aesop
+  | zero => exact Commute.zero_left _
+  | add _ _ _ _ h₁ h₂ => exact h₁.add_left h₂
+  | smul _ _ _ h => exact h.smul_left _
+
+/-- If every element of a set `s` commutes with `x`, then every element of `Submodule.span R s`
+commutes with `x`. -/
+theorem Commute.span_right {s : Set M} {x : M} (h : ∀ y ∈ s, Commute x y) :
+    ∀ y ∈ Submodule.span R s, Commute x y := by
+  simp only [Commute.symm_iff (a := x)] at *
+  exact Commute.span_left h
+
+end CommuteSpan

LeanOA/Mathlib/Algebra/Star/Unitary.lean

@@ -0,0 +1,35 @@
+module
+
+public import Mathlib.Algebra.Star.Unitary
+
+public section Unitary
+
+variable {R : Type*} [Monoid R] [StarMul R]
+
+lemma Unitary.commute_self_star (u : unitary R) : Commute u (star u) := by simp [commute_iff_eq]
+lemma Unitary.commute_star_self (u : unitary R) : Commute (star u) u := by simp [commute_iff_eq]
+
+lemma commute_unitary_self_star {u : R} (hu : u ∈ unitary R) : Commute u (star u) := by
+  simpa only [commute_iff_eq, Subtype.ext_iff, Submonoid.coe_mul, Unitary.coe_star] using
+    Unitary.commute_self_star ⟨u, hu⟩
+
+lemma commute_unitary_star_self {u : R} (hu : u ∈ unitary R) : Commute (star u) u :=
+  commute_unitary_self_star hu |>.symm
+
+lemma commute_unitary_iff_star_mul_mul {x : R} {u : unitary R} :
+    Commute (u : R) x ↔ star u * x * u = x := by
+  simpa using (Unitary.toUnits u).commute_iff_inv_mul_cancel
+
+lemma commute_unitary_iff_star_mul_mul_of_mem {x u : R} {hu : u ∈ unitary R} :
+    Commute (u : R) x ↔ star u * x * u = x :=
+  commute_unitary_iff_star_mul_mul (u := ⟨u, hu⟩)
+
+lemma commute_unitary_iff_mul_mul_star {x : R} {u : unitary R} :
+    Commute (u : R) x ↔ u * x * star u = x := by
+  simpa using (Unitary.toUnits u).commute_iff_mul_inv_cancel
+
+lemma commute_unitary_iff_mul_mul_star_of_mem {x u : R} {hu : u ∈ unitary R} :
+    Commute (u : R) x ↔ u * x * star u = x :=
+  commute_unitary_iff_mul_mul_star (u := ⟨u, hu⟩)
+
+end Unitary

LeanOA/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2025 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
+
+/- The primed versions of these lemmas should replace the originals in Mathlib. -/
+
+
+public section
+
+section Unital
+
+section RCLike
+
+variable (𝕜 : Type*) {A : Type*} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A]
+variable [TopologicalSpace A] [StarModule 𝕜 A]
+variable [ContinuousFunctionalCalculus 𝕜 A p]
+variable [IsTopologicalRing A] [ContinuousStar A]
+
+open StarAlgebra
+
+open scoped ContinuousFunctionalCalculus in
+theorem range_cfcHom_le {a : A} (ha : p a) :
+    (cfcHom ha (R := 𝕜)).range ≤ elemental 𝕜 a := by
+  grw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental,
+    StarSubalgebra.map_topologicalClosure_le _ _ (cfcHom_continuous ha (R := 𝕜)),
+    StarAlgHom.map_adjoin]
+  simp [cfcHom_id ha, elemental]
+
+lemma range_cfc_subset {a : A} (ha : p a) : Set.range (cfc (R := 𝕜) · a) ⊆ elemental 𝕜 a := by
+  grw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom_le 𝕜 ha]
+
+variable {𝕜}
+
+theorem cfcHom_apply_mem_elemental' {a : A} (ha : p a) (f : C(spectrum 𝕜 a, 𝕜)) :
+    cfcHom ha f ∈ elemental 𝕜 a :=
+  range_cfcHom_le 𝕜 ha ⟨f, rfl⟩
+
+@[simp, grind ←]
+theorem cfc_apply_mem_elemental' (f : 𝕜 → 𝕜) (a : A) :
+    cfc f a ∈ elemental 𝕜 a :=
+  cfc_cases _ a f (zero_mem _) fun hf ha ↦
+    cfcHom_apply_mem_elemental' ha ⟨_, hf.restrict⟩
+
+lemma cfc_mem {S : Type*} [SetLike S A] [SubringClass S A] [SMulMemClass S 𝕜 A]
+    [StarMemClass S A] (s : S) [IsClosed (s : Set A)] (f : 𝕜 → 𝕜) (a : A) (has : a ∈ s) :
+    cfc f a ∈ s :=
+  StarSubalgebra.topologicalClosure_minimal (t := .ofClass s) (by simpa) (by simpa)
+    (cfc_apply_mem_elemental' f a)
+
+-- this should probably be an instance?
+attribute [instance] StarAlgebra.elemental.isClosed
+
+end RCLike
+
+open scoped NNReal
+variable {A : Type*} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A]
+variable [ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A]
+variable [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A]
+
+lemma range_cfc_nnreal_eq_image_cfc_real' (a : A) (ha : 0 ≤ a) :
+    Set.range (cfc (R := ℝ≥0) · a) = (cfc · a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} := by
+  ext
+  constructor
+  · rintro ⟨f, rfl⟩
+    simp only [cfc_nnreal_eq_real f a ha]
+    exact ⟨_, fun _ _ ↦ by positivity, rfl⟩
+  · rintro ⟨f, hf, rfl⟩
+    simp only [cfc_real_eq_nnreal a hf]
+    exact ⟨_, rfl⟩
+
+variable [ContinuousStar A] [StarModule ℝ A]
+
+lemma range_cfc_nnreal' (a : A) (ha : 0 ≤ a) :
+    Set.range (cfc (R := ℝ≥0) · a) ⊆ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x} := by
+  grw [range_cfc_nnreal_eq_image_cfc_real' a ha, Set.setOf_and, SetLike.setOf_mem_eq,
+    ← range_cfc_subset ℝ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
+  exact Set.image_mono fun _ ↦ cfc_nonneg
+
+end Unital
+
+section NonUnital
+
+section RCLike
+
+variable (𝕜 : Type*) {A : Type*} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A]
+variable [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A]
+variable [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p]
+variable [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A]
+
+open NonUnitalStarAlgebra
+
+open scoped NonUnitalContinuousFunctionalCalculus in
+theorem range_cfcₙHom_le {a : A} (ha : p a) :
+    NonUnitalStarAlgHom.range (cfcₙHom ha (R := 𝕜)) ≤ elemental 𝕜 a := by
+  grw [← NonUnitalStarAlgebra.map_top, ← ContinuousMapZero.elemental_eq_top,
+    NonUnitalStarAlgebra.elemental,
+    NonUnitalStarSubalgebra.map_topologicalClosure_le (R := 𝕜) _ (cfcₙHom_continuous ha),
+    NonUnitalStarAlgHom.map_adjoin]
+  simp [cfcₙHom_id ha, elemental]
+
+theorem range_cfcₙ_subset {a : A} (ha : p a) : Set.range (cfcₙ (R := 𝕜) · a) ⊆ elemental 𝕜 a := by
+  grw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom_le 𝕜 ha]
+
+variable {𝕜}
+
+open scoped ContinuousMapZero
+
+theorem cfcₙHom_apply_mem_elemental' {a : A} (ha : p a) (f : C(quasispectrum 𝕜 a, 𝕜)₀) :
+    cfcₙHom ha f ∈ elemental 𝕜 a :=
+  range_cfcₙHom_le 𝕜 ha ⟨f, rfl⟩
+
+@[simp, grind ←]
+theorem cfcₙ_apply_mem_elemental' (f : 𝕜 → 𝕜) (a : A) :
+    cfcₙ f a ∈ elemental 𝕜 a :=
+  cfcₙ_cases _ a f (zero_mem _) fun hf hf₀ ha ↦
+    cfcₙHom_apply_mem_elemental' ha ⟨⟨_, hf.restrict⟩, hf₀⟩
+
+lemma cfcₙ_mem {S : Type*} [SetLike S A] [NonUnitalSubringClass S A] [SMulMemClass S 𝕜 A]
+    [StarMemClass S A] (s : S) [IsClosed (s : Set A)] (f : 𝕜 → 𝕜) (a : A) (has : a ∈ s) :
+    cfcₙ f a ∈ s :=
+  NonUnitalStarSubalgebra.topologicalClosure_minimal (t := .ofClass s) _ (by simpa) (by simpa)
+    (cfcₙ_apply_mem_elemental' f a)
+
+end RCLike
+
+open scoped NNReal
+variable {A : Type*} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A]
+variable [SMulCommClass ℝ A A] [TopologicalSpace A]
+variable [NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
+variable [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A]
+variable [StarOrderedRing A]
+
+lemma range_cfcₙ_nnreal_eq_image_cfcₙ_real' (a : A) (ha : 0 ≤ a) :
+    Set.range (cfcₙ (R := ℝ≥0) · a) = (cfcₙ · a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} := by
+  ext
+  constructor
+  · rintro ⟨f, rfl⟩
+    simp only [cfcₙ_nnreal_eq_real f a]
+    exact ⟨_, fun _ _ ↦ by positivity, rfl⟩
+  · rintro ⟨f, hf, rfl⟩
+    simp only [cfcₙ_real_eq_nnreal a hf]
+    exact ⟨_, rfl⟩
+
+variable [StarModule ℝ A] [ContinuousStar A] [ContinuousConstSMul ℝ A]
+
+lemma range_cfcₙ_nnreal' (a : A) (ha : 0 ≤ a) :
+    Set.range (cfcₙ (R := ℝ≥0) · a) ⊆ {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x} := by
+  grw [range_cfcₙ_nnreal_eq_image_cfcₙ_real' a ha, Set.setOf_and, SetLike.setOf_mem_eq,
+    ← range_cfcₙ_subset _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
+  exact Set.image_mono fun _ ↦ cfcₙ_nonneg
+
+end NonUnital

LeanOA/Mathlib/Analysis/RCLike/ContinuousMap.lean

@@ -3,7 +3,7 @@ import Mathlib.Topology.ContinuousMap.Compact
 import Mathlib.Topology.ContinuousMap.Ordered
 import Mathlib.Topology.ContinuousMap.Units
 
-variable {A Y 𝕜 : Type*} [RCLike 𝕜] [TopologicalSpace A] [TopologicalSpace Y]
+variable {A 𝕜 : Type*} [RCLike 𝕜] [TopologicalSpace A]
 
 namespace ContinuousMap
 
@@ -18,11 +18,6 @@ variable (𝕜) in
     spectrum ℝ (f.realToRCLike 𝕜) = spectrum ℝ f := by
   ext; simp [spectrum.mem_iff, isUnit_iff_forall_isUnit, RCLike.ext_iff (K := 𝕜), Algebra.smul_def]
 
-variable (A 𝕜) in
-open ComplexOrder in
-lemma monotone_realToRCLike : Monotone (realToRCLike (A := A) 𝕜) :=
-  fun f g hfg x ↦ by simpa using hfg x
-
 /-- Mapping `C(A, 𝕜)` to `C(A, ℝ)` using `RCLike.re`. -/
 @[simps] def rclikeToReal (f : C(A, 𝕜)) : C(A, ℝ) where toFun x := RCLike.re (f x)
 
@@ -47,4 +42,40 @@ variable (𝕜) in
 @[simp] theorem isometry_realToRCLike [CompactSpace A] : Isometry (realToRCLike 𝕜 (A := A)) :=
   .of_dist_eq fun f g ↦ by simp [dist_eq_norm, norm_eq_iSup_norm, ← map_sub]
 
+open scoped ComplexOrder
+
+variable (𝕜)
+
+/-- `ContinuousMap.realToRCLike` as an order embedding. -/
+def realToRCLikeOrderEmbedding :
+    C(A, ℝ) ↪o C(A, 𝕜) where
+  toFun := realToRCLike 𝕜
+  inj' f g hfg := by ext x; simpa using congr($hfg x)
+  map_rel_iff' := by simp [le_def]
+
+variable (A) in
+lemma realToRCLike_monotone : Monotone (realToRCLike (A := A) 𝕜) :=
+  realToRCLikeOrderEmbedding 𝕜 |>.monotone
+
+lemma realToRCLike_strictMono : StrictMono (realToRCLike (A := A) 𝕜) :=
+  realToRCLikeOrderEmbedding 𝕜 |>.strictMono
+
+@[simp]
+lemma realToRCLike_injective : (realToRCLike (A := A) 𝕜).Injective :=
+  realToRCLikeOrderEmbedding 𝕜 |>.injective
+
+@[simp]
+lemma realToRCLike_inj {f g : C(A, ℝ)} : realToRCLike 𝕜 f = realToRCLike 𝕜 g ↔ f = g :=
+  realToRCLikeOrderEmbedding 𝕜 |>.eq_iff_eq
+
+@[simp]
+lemma realToRCLike_le_realToRCLike_iff {f g : C(A, ℝ)} :
+    realToRCLike 𝕜 f ≤ realToRCLike 𝕜 g ↔ f ≤ g :=
+  realToRCLikeOrderEmbedding 𝕜 |>.le_iff_le
+
+@[simp]
+lemma realToRCLike_lt_realToRCLike_iff {f g : C(A, ℝ)} :
+    realToRCLike 𝕜 f < realToRCLike 𝕜 g ↔ f < g :=
+  realToRCLikeOrderEmbedding 𝕜 |>.lt_iff_lt
+
 end ContinuousMap