α : Type ?u.48758
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : x ∈ pi univ s
y : (i : β) → π i
hy : y ∈ pi univ s
hxy : x ≠ y
⊢ c ≤ edist x y
α : Type ?u.48758
β : Type u_2
inst✝² : PseudoEMetricSpace α
x y z : α
s✝ t : Set α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
⊢ c ≤ einfsep (pi univ s)
refine' le_einfsep fun x hx y hy hxy => _
α : Type ?u.48758
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y
α : Type ?u.48758
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : x ∈ pi univ s
y : (i : β) → π i
hy : y ∈ pi univ s
hxy : x ≠ y
⊢ c ≤ edist x y
rw [mem_univ_pi] at hx hy
case intro
α : Type ?u.48758
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y
α : Type ?u.48758
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y
rcases Function.ne_iff.mp hxy with ⟨i, hi⟩
no goals
case intro
α : Type ?u.48758
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y
exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)