case intro.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ (⋃ (n : ℕ), F n) = U ∧ Monotone F
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ (⋃ (n : ℕ), F n) = U ∧ Monotone F
obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one
case intro.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ (⋃ (n : ℕ), F n) = U ∧ Monotone F
case intro.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ (⋃ (n : ℕ), F n) = U ∧ Monotone F
let F := fun n : ℕ => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
case intro.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ (⋃ (n : ℕ), F n) = U ∧ Monotone F
case intro.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ (⋃ (n : ℕ), F n) = U ∧ Monotone F
have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
  by_contra h
  have : infEdist x (Uᶜ) ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
  exact this (infEdist_zero_of_mem h)
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ (⋃ (n : ℕ), F n) = U

case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
case intro.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ (⋃ (n : ℕ), F n) = U ∧ Monotone F
refine ⟨F, fun n => IsClosed.preimage continuous_infEdist isClosed_Ici, F_subset, ?_, ?_⟩
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ (⋃ (n : ℕ), F n) = U

case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ (⋃ (n : ℕ), F n) = U

case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
show (⋃ n, F n) = U
case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
show Monotone F
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : ¬x ∈ U
⊢ False
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
⊢ x ∈ U
by_contra h
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : ¬x ∈ U
this : infEdist x (Uᶜ) ≠ 0
⊢ False
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : ¬x ∈ U
⊢ False
have : infEdist x (Uᶜ) ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
no goals
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : ¬x ∈ U
this : infEdist x (Uᶜ) ≠ 0
⊢ False
exact this (infEdist_zero_of_mem h)
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ x ∈ ⋃ (n : ℕ), F n
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ (⋃ (n : ℕ), F n) = U
refine' Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => _
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬x ∈ Uᶜ
⊢ x ∈ ⋃ (n : ℕ), F n
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ x ∈ ⋃ (n : ℕ), F n
have : ¬x ∈ Uᶜ := by simpa using hx
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x (Uᶜ) = 0
⊢ x ∈ ⋃ (n : ℕ), F n
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬x ∈ Uᶜ
⊢ x ∈ ⋃ (n : ℕ), F n
rw [mem_iff_infEdist_zero_of_closed hU.isClosed_compl] at this
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
⊢ x ∈ ⋃ (n : ℕ), F n
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x (Uᶜ) = 0
⊢ x ∈ ⋃ (n : ℕ), F n
have B : 0 < infEdist x (Uᶜ) := by simpa [pos_iff_ne_zero] using this
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
⊢ x ∈ ⋃ (n : ℕ), F n
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
⊢ x ∈ ⋃ (n : ℕ), F n
have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) :=
  ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 a_lt_one
case intro.intro.refine_1.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEdist x (Uᶜ)
⊢ x ∈ ⋃ (n : ℕ), F n
case intro.intro.refine_1
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
⊢ x ∈ ⋃ (n : ℕ), F n
rcases((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
case intro.intro.refine_1.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEdist x (Uᶜ)
⊢ ∃ i, a ^ i ≤ infEdist x (Uᶜ)
case intro.intro.refine_1.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEdist x (Uᶜ)
⊢ x ∈ ⋃ (n : ℕ), F n
simp only [mem_iUnion, mem_Ici, mem_preimage]
no goals
case intro.intro.refine_1.intro
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x (Uᶜ) = 0
B : 0 < infEdist x (Uᶜ)
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEdist x (Uᶜ)
⊢ ∃ i, a ^ i ≤ infEdist x (Uᶜ)
exact ⟨n, hn.le⟩
no goals
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ (⋃ (n : ℕ), F n) ⊆ U
simp only [iUnion_subset_iff, F_subset, forall_const]
no goals
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ ¬x ∈ Uᶜ
simpa using hx
no goals
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x (Uᶜ) = 0
⊢ 0 < infEdist x (Uᶜ)
simpa [pos_iff_ne_zero] using this
case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
m n : ℕ
hmn : m ≤ n
x : α
hx : x ∈ F m
⊢ x ∈ F n
case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
intro m n hmn x hx
case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
m n : ℕ
hmn : m ≤ n
x : α
hx : a ^ m ≤ infEdist x (Uᶜ)
⊢ a ^ n ≤ infEdist x (Uᶜ)
case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
m n : ℕ
hmn : m ≤ n
x : α
hx : x ∈ F m
⊢ x ∈ F n
simp only [mem_Ici, mem_preimage] at hx⊢
no goals
case intro.intro.refine_2
ι : Sort ?u.21246
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x (Uᶜ)) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
m n : ℕ
hmn : m ≤ n
x : α
hx : a ^ m ≤ infEdist x (Uᶜ)
⊢ a ^ n ≤ infEdist x (Uᶜ)
apply le_trans (pow_le_pow_of_le_one' a_lt_one.le hmn) hx