[GOAL]
α : Type u_1
inst✝² : NormedAddCommGroup α
inst✝¹ : Lattice α
inst✝ : HasSolidNorm α
x✝² x✝¹ : ℚ
x✝ : |x✝²| ≤ |x✝¹|
⊢ ‖x✝²‖ ≤ ‖x✝¹‖
[PROOFSTEP]
simpa only [norm, ← Rat.cast_abs, Rat.cast_le]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ ‖a‖ ≤ ‖b‖
[PROOFSTEP]
apply solid
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ |a| ≤ |b|
[PROOFSTEP]
rw [abs_eq_sup_neg]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ a ⊔ -a ≤ |b|
[PROOFSTEP]
nth_rw 1 [← neg_neg a]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ - -a ⊔ -a ≤ |b|
[PROOFSTEP]
rw [← neg_inf_eq_sup_neg]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ |b|
[PROOFSTEP]
rw [abs_eq_sup_neg]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ b ⊔ -b
[PROOFSTEP]
nth_rw 1 [← neg_neg b]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b
[PROOFSTEP]
rwa [← neg_inf_eq_sup_neg, neg_le_neg_iff, @inf_comm _ _ _ b, @inf_comm _ _ _ a]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
[PROOFSTEP]
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
[PROOFSTEP]
refine' le_trans (solid _) (norm_add_le |a - c| |b - d|)
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||
[PROOFSTEP]
rw [abs_of_nonneg (|a - c| + |b - d|) (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
calc
  |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)| := by rw [sub_add_sub_cancel]
  _ ≤ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| := (abs_add_le _ _)
  _ ≤ |a - c| + |b - d| := by
    apply add_le_add
    · exact abs_inf_sub_inf_le_abs _ _ _
    · rw [@inf_comm _ _ c, @inf_comm _ _ c]
      exact abs_inf_sub_inf_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
apply add_le_add
[GOAL]
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| ≤ |a - c|
[PROOFSTEP]
exact abs_inf_sub_inf_le_abs _ _ _
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|
[PROOFSTEP]
rw [@inf_comm _ _ c, @inf_comm _ _ c]
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|
[PROOFSTEP]
exact abs_inf_sub_inf_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
[PROOFSTEP]
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
[PROOFSTEP]
refine' le_trans (solid _) (norm_add_le |a - c| |b - d|)
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||
[PROOFSTEP]
rw [abs_of_nonneg (|a - c| + |b - d|) (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
calc
  |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)| := by rw [sub_add_sub_cancel]
  _ ≤ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| := (abs_add_le _ _)
  _ ≤ |a - c| + |b - d| := by
    apply add_le_add
    · exact abs_sup_sub_sup_le_abs _ _ _
    · rw [@sup_comm _ _ c, @sup_comm _ _ c]
      exact abs_sup_sub_sup_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
apply add_le_add
[GOAL]
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|
[PROOFSTEP]
exact abs_sup_sub_sup_le_abs _ _ _
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|
[PROOFSTEP]
rw [@sup_comm _ _ c, @sup_comm _ _ c]
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|
[PROOFSTEP]
exact abs_sup_sub_sup_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
have h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_inf_sub_inf_le_add_norm x y 0 0
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
simpa only [inf_idem, sub_zero] using h
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
have h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_sup_sub_sup_le_add_norm x y 0 0
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
simpa only [sup_idem, sub_zero] using h
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
⊢ ContinuousInf α
[PROOFSTEP]
refine' ⟨continuous_iff_continuousAt.2 fun q => tendsto_iff_norm_tendsto_zero.2 <| _⟩
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
⊢ Filter.Tendsto (fun e => ‖e.fst ⊓ e.snd - (fun p => p.fst ⊓ p.snd) q‖) (nhds q) (nhds 0)
[PROOFSTEP]
have : ∀ p : α × α, ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖ := fun _ => norm_inf_sub_inf_le_add_norm _ _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
this : ∀ (p : α × α), ‖p.fst ⊓ p.snd - q.fst ⊓ q.snd‖ ≤ ‖p.fst - q.fst‖ + ‖p.snd - q.snd‖
⊢ Filter.Tendsto (fun e => ‖e.fst ⊓ e.snd - (fun p => p.fst ⊓ p.snd) q‖) (nhds q) (nhds 0)
[PROOFSTEP]
refine' squeeze_zero (fun e => norm_nonneg _) this _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
this : ∀ (p : α × α), ‖p.fst ⊓ p.snd - q.fst ⊓ q.snd‖ ≤ ‖p.fst - q.fst‖ + ‖p.snd - q.snd‖
⊢ Filter.Tendsto (fun t => ‖t.fst - q.fst‖ + ‖t.snd - q.snd‖) (nhds q) (nhds 0)
[PROOFSTEP]
convert
  ((continuous_fst.tendsto q).sub <| tendsto_const_nhds).norm.add
    ((continuous_snd.tendsto q).sub <| tendsto_const_nhds).norm
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
this : ∀ (p : α × α), ‖p.fst ⊓ p.snd - q.fst ⊓ q.snd‖ ≤ ‖p.fst - q.fst‖ + ‖p.snd - q.snd‖
⊢ 0 = ‖q.fst - q.fst‖ + ‖q.snd - q.snd‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ ↑1 * dist x y
[PROOFSTEP]
rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
[PROOFSTEP]
exact norm_sup_sub_sup_le_norm x y z
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
⊢ Continuous NegPart.neg
[PROOFSTEP]
refine continuous_pos.comp <| @continuous_neg _ _ _ TopologicalAddGroup.toContinuousNeg
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
⊢ IsClosed {x | 0 ≤ x}
[PROOFSTEP]
suffices {x : E | 0 ≤ x} = NegPart.neg ⁻¹' {(0 : E)} by
  rw [this]
  exact IsClosed.preimage continuous_neg' isClosed_singleton
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
this : {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
⊢ IsClosed {x | 0 ≤ x}
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
this : {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
⊢ IsClosed (NegPart.neg ⁻¹' {0})
[PROOFSTEP]
exact IsClosed.preimage continuous_neg' isClosed_singleton
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
⊢ {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
x : E
⊢ x ∈ {x | 0 ≤ x} ↔ x ∈ NegPart.neg ⁻¹' {0}
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_setOf_eq,
  @neg_eq_zero_iff E _ _ (OrderedAddCommGroup.to_covariantClass_left_le E)]
  -- porting note: I'm not sure why Lean couldn't synthesize this instance because it works with
    -- `have : CovariantClass E E (· + ·) (· ≤ ·) := inferInstance`
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ IsClosed {p | p.fst ≤ p.snd}
[PROOFSTEP]
have : {p : G × G | p.fst ≤ p.snd} = (fun p : G × G => p.snd - p.fst) ⁻¹' {x : G | 0 ≤ x} := by ext1 p;
  simp only [sub_nonneg, Set.preimage_setOf_eq]
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
[PROOFSTEP]
ext1 p
[GOAL]
case h
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.fst ≤ p.snd} ↔ p ∈ (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
[PROOFSTEP]
simp only [sub_nonneg, Set.preimage_setOf_eq]
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed {p | p.fst ≤ p.snd}
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed ((fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x})
[PROOFSTEP]
exact IsClosed.preimage (continuous_snd.sub continuous_fst) h
