case inl
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded s

case inr
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : Set.Nonempty s
⊢ TotallyBounded s
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ TotallyBounded s
cases' s.eq_empty_or_nonempty with hs hs
case inr.intro
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
⊢ TotallyBounded s
case inr
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : Set.Nonempty s
⊢ TotallyBounded s
rcases hs with ⟨x0, hx0⟩
case inr.intro
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
⊢ TotallyBounded s
case inr.intro
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
⊢ TotallyBounded s
haveI : Inhabited s := ⟨⟨x0, hx0⟩⟩
case inr.intro
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
case inr.intro
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
⊢ TotallyBounded s
refine' totallyBounded_iff.2 fun ε ε0 => _
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
case inr.intro
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
rcases H ε ε0 with ⟨β, fβ, F, hF⟩
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
let Finv := Function.invFun F
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range (Subtype.val ∘ Finv)), ball y ε
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
refine' ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => _⟩
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F { val := x, property := xs })
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range (Subtype.val ∘ Finv)), ball y ε
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range (Subtype.val ∘ Finv)), ball y ε
let x' := Finv (F ⟨x, xs⟩)
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F { val := x, property := xs })
this : F x' = F { val := x, property := xs }
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range (Subtype.val ∘ Finv)), ball y ε
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F { val := x, property := xs })
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range (Subtype.val ∘ Finv)), ball y ε
have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F { val := x, property := xs })
this : F x' = F { val := x, property := xs }
⊢ ∃ i i_1, x ∈ ball i ε
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F { val := x, property := xs })
this : F x' = F { val := x, property := xs }
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range (Subtype.val ∘ Finv)), ball y ε
simp only [Set.mem_iUnion, Set.mem_range]
no goals
case inr.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F { val := x, property := xs })
this : F x' = F { val := x, property := xs }
⊢ ∃ i i_1, x ∈ ball i ε
exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩
case inl
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded ∅
case inl
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded s
rw [hs]
no goals
case inl
α : Type u
β : Type v
X : Type ?u.63903
ι : Type ?u.63906
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded ∅
exact totallyBounded_empty