α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ HasBasis (𝓤 α) p fun x => {p | edist p.fst p.snd ≤ f x}
refine' ⟨fun s => uniformity_basis_edist.mem_iff.trans _⟩
case mp
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s

case mpr
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
constructor
case mp.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
case mp
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
rintro ⟨ε, ε₀, hε⟩
case mp.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
case mp.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
rcases exists_between ε₀ with ⟨ε', hε'⟩
case mp.intro.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
case mp.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
rcases hf ε' hε'.1 with ⟨i, hi, H⟩
no goals
case mp.intro.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
exact ⟨i, hi, fun x hx => hε <| lt_of_le_of_lt (le_trans hx.out H) hε'.2⟩
no goals
case mpr
α : Type u
β✝ : Type v
X : Type ?u.17483
inst✝ : PseudoEMetricSpace α
β : Type u_1
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩