case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ↑f)
⊢ BddAbove (range fun y => ⨅ (x : X), ↑f (inl x, inr y) + C)
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f : GromovHausdorff.Cb X Y
C : ℝ
⊢ BddAbove (range fun y => ⨅ (x : X), ↑f (inl x, inr y) + C)
rcases (Real.bounded_iff_bddBelow_bddAbove.1 f.bounded_range).2 with ⟨Cf, hCf⟩
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y✝ z t : X ⊕ Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ↑f)
y : Y
⊢ (⨅ (x : X), ↑f (inl x, inr y) + C) ≤ Cf + C
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ↑f)
⊢ BddAbove (range fun y => ⨅ (x : X), ↑f (inl x, inr y) + C)
refine' ⟨Cf + C, forall_range_iff.2 fun y => _⟩
no goals
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y✝ z t : X ⊕ Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ↑f)
y : Y
⊢ (⨅ (x : X), ↑f (inl x, inr y) + C) ≤ Cf + C
calc
  (⨅ x, f (inl x, inr y) + C) ≤ f (inl default, inr y) + C := ciInf_le (HD_below_aux2 C) default
  _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl