feat(topology/continuous_map): formulas for sup and inf in terms of abs (#6720)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/ordered_group.lean

@@ -683,6 +683,20 @@ section linear_ordered_add_comm_group
 
 variables [linear_ordered_add_comm_group α] {a b c : α}
 
+@[simp]
+lemma sub_le_sub_flip : a - b ≤ b - a ↔ a ≤ b :=
+begin
+  rw [sub_le_iff_le_add, sub_add_eq_add_sub, le_sub_iff_add_le],
+  split,
+  { intro h,
+    by_contra H,
+    rw not_le at H,
+    apply not_lt.2 h,
+    exact add_lt_add H H, },
+  { intro h,
+    exact add_le_add h h, }
+end
+
 lemma le_of_forall_pos_le_add [densely_ordered α] (h : ∀ ε : α, 0 < ε → a ≤ b + ε) : a ≤ b :=
 le_of_forall_le_of_dense $ λ c hc,
 calc a ≤ b + (c - b) : h _ (sub_pos_of_lt hc)

src/topology/algebra/continuous_functions.lean

@@ -120,6 +120,12 @@ instance continuous_map_group {α : Type*} {β : Type*} [topological_space α] [
   mul_left_inv := λ a, by ext; exact mul_left_inv _,
   ..continuous_map_monoid }
 
+@[simp, norm_cast, to_additive]
+lemma div_coe {α : Type*} {β : Type*} [topological_space α] [topological_space β]
+  [group β] [topological_group β] (f g : C(α, β)) :
+  ((f / g : C(α, β)) : α → β) = (f : α → β) / (g : α → β) :=
+by { simp only [div_eq_mul_inv], refl, }
+
 @[to_additive]
 instance continuous_map_comm_group {α : Type*} {β : Type*} [topological_space α]
   [topological_space β] [comm_group β] [topological_group β] : comm_group C(α, β) :=
@@ -372,3 +378,49 @@ instance continuous_map_module' {α : Type*} [topological_space α]
 end continuous_map
 
 end module_over_continuous_functions
+
+/-!
+We now provide formulas for `f ⊓ g` and `f ⊔ g`, where `f g : C(α, β)`,
+in terms of `continuous_map.abs`.
+-/
+
+section
+variables {R : Type*} [linear_ordered_field R]
+
+-- TODO:
+-- This lemma (and the next) could go all the way back in `algebra.ordered_field`,
+-- except that it is tedious to prove without tactics.
+-- Rather than stranding it at some intermediate location,
+-- it's here, immediately prior to the point of use.
+lemma min_eq_half_add_sub_abs_sub {x y : R} : min x y = 2⁻¹ * (x + y - abs (x - y)) :=
+begin
+  dsimp [min, max, abs],
+  simp only [neg_le_self_iff, if_congr, sub_nonneg, neg_sub],
+  split_ifs; ring; linarith,
+end
+
+lemma max_eq_half_add_add_abs_sub {x y : R} : max x y = 2⁻¹ * (x + y + abs (x - y)) :=
+begin
+  dsimp [min, max, abs],
+  simp only [neg_le_self_iff, if_congr, sub_nonneg, neg_sub],
+  split_ifs; ring; linarith,
+end
+end
+
+namespace continuous_map
+
+section lattice
+variables {α : Type*} [topological_space α]
+variables {β : Type*} [linear_ordered_field β] [topological_space β]
+  [order_topology β] [topological_ring β]
+
+lemma inf_eq (f g : C(α, β)) : f ⊓ g = (2⁻¹ : β) • (f + g - (f - g).abs) :=
+ext (λ x, by simpa using min_eq_half_add_sub_abs_sub)
+
+-- Not sure why this is grosser than `inf_eq`:
+lemma sup_eq (f g : C(α, β)) : f ⊔ g = (2⁻¹ : β) • (f + g + (f - g).abs) :=
+ext (λ x, by simpa [mul_add] using @max_eq_half_add_add_abs_sub _ _ (f x) (g x))
+
+end lattice
+
+end continuous_map

src/topology/continuous_map.lean

@@ -83,6 +83,18 @@ def const (b : β) : C(α, β) := ⟨λ x, b⟩
 @[simp] lemma const_coe (b : β) : (const b : α → β) = (λ x, b) := rfl
 lemma const_apply (b : β) (a : α) : const b a = b := rfl
 
+section
+variables [linear_ordered_add_comm_group β] [order_topology β]
+
+/-- The pointwise absolute value of a continuous function as a continuous function. -/
+def abs (f : C(α, β)) : C(α, β) :=
+{ to_fun := λ x, abs (f x), }
+
+@[simp] lemma abs_apply (f : C(α, β)) (x : α) : f.abs x = _root_.abs (f x) :=
+rfl
+
+end
+
 /-!
 We now set up the partial order and lattice structure (given by pointwise min and max)
 on continuous functions.