α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.fst p.snd < i} ⊆ s) ↔ ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
⊢ HasBasis (𝓤 α) p fun i => {p | dist p.fst p.snd < f i}
refine' ⟨fun s => uniformity_basis_dist.mem_iff.trans _⟩
case mp
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.fst p.snd < i} ⊆ s) → ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s

case mpr
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | dist p.fst p.snd < i} ⊆ s
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.fst p.snd < i} ⊆ s) ↔ ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s
constructor
case mp.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.fst p.snd < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s
case mp
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.fst p.snd < i} ⊆ s) → ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s
rintro ⟨ε, ε₀, hε⟩
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.fst p.snd < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s
case mp.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.fst p.snd < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s
rcases hf ε₀ with ⟨i, hi, H⟩
no goals
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.fst p.snd < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s
exact ⟨i, hi, fun x (hx : _ < _) => hε <| lt_of_lt_of_le hx H⟩
no goals
case mpr
α : Type u
β✝ : Type v
X : Type ?u.49504
ι : Type ?u.49507
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
β : Type u_1
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | dist p.fst p.snd < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | dist p.fst p.snd < i} ⊆ s
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩