case mp
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
⊢ TotallyBounded s → ∀ (f : Filter α), NeBot f → f ≤ 𝓟 s → ∃ c, c ≤ f ∧ Cauchy c

case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (f : Filter α), NeBot f → f ≤ 𝓟 s → ∃ c, c ≤ f ∧ Cauchy c) → TotallyBounded s
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ (f : Filter α), NeBot f → f ≤ 𝓟 s → ∃ c, c ≤ f ∧ Cauchy c
constructor
no goals
case mp
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
⊢ TotallyBounded s → ∀ (f : Filter α), NeBot f → f ≤ 𝓟 s → ∃ c, c ≤ f ∧ Cauchy c
exact fun H f hf hfs => ⟨Ultrafilter.of f, Ultrafilter.of_le f,
  (Ultrafilter.of f).cauchy_of_totallyBounded H ((Ultrafilter.of_le f).trans hfs)⟩
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (f : Filter α), NeBot f → f ≤ 𝓟 s → ∃ c, c ≤ f ∧ Cauchy c
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (f : Filter α), NeBot f → f ≤ 𝓟 s → ∃ c, c ≤ f ∧ Cauchy c) → TotallyBounded s
intro H d hd
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
⊢ ∃ f, NeBot f ∧ f ≤ 𝓟 s ∧ ∀ (c : Filter α), c ≤ f → ¬Cauchy c
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
H : ∀ (f : Filter α), NeBot f → f ≤ 𝓟 s → ∃ c, c ≤ f ∧ Cauchy c
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
contrapose! H with hd_cover
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
⊢ ∃ f, NeBot f ∧ f ≤ 𝓟 s ∧ ∀ (c : Filter α), c ≤ f → ¬Cauchy c
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
⊢ ∃ f, NeBot f ∧ f ≤ 𝓟 s ∧ ∀ (c : Filter α), c ≤ f → ¬Cauchy c
set f := ⨅ t : Finset α, 𝓟 (s \ ⋃ y ∈ t, { x | (x, y) ∈ d })
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
⊢ ∃ f, NeBot f ∧ f ≤ 𝓟 s ∧ ∀ (c : Filter α), c ≤ f → ¬Cauchy c
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this : NeBot f
⊢ ∃ f, NeBot f ∧ f ≤ 𝓟 s ∧ ∀ (c : Filter α), c ≤ f → ¬Cauchy c
have : f ≤ 𝓟 s := iInf_le_of_le ∅ (by simp)
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
⊢ False
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
⊢ ∃ f, NeBot f ∧ f ≤ 𝓟 s ∧ ∀ (c : Filter α), c ≤ f → ¬Cauchy c
refine' ⟨f, ‹_›, ‹_›, fun c hcf hc => _⟩
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
⊢ False
case mpr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
⊢ False
rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ False
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
⊢ False
rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
⊢ False
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ False
set ys := ⋃ y' ∈ ({y} : Finset α), { x | (x, y') ∈ d }
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
⊢ False
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝ : NeBot f
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
⊢ False
have : c ≤ 𝓟 (s \ ys) := hcf.trans (iInf_le_of_le {y} le_rfl)
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
⊢ ∅ ∈ c
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
⊢ False
refine' hc.1.ne (empty_mem_iff_bot.mp _)
case h
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
⊢ ∀ (a : α), (a ∈ s \ ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}) → a ∈ m → a ∈ ∅
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
⊢ ∅ ∈ c
filter_upwards [le_principal_iff.1 this, hm]
case h
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
x : α
hx : x ∈ s \ ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
hxm : x ∈ m
⊢ x ∈ ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
case h
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
⊢ ∀ (a : α), (a ∈ s \ ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}) → a ∈ m → a ∈ ∅
refine' fun x hx hxm => hx.2 _
no goals
case h
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this✝¹ : NeBot f
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
ys : Set α := ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
this : c ≤ 𝓟 (s \ ys)
x : α
hx : x ∈ s \ ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
hxm : x ∈ m
⊢ x ∈ ⋃ (y' : α) (_ : y' ∈ {y}), {x | (x, y') ∈ d}
simpa using hmd (mk_mem_prod hxm hym)
case refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
⊢ ∀ ⦃i j : Finset α⦄,
    i ≤ j → 𝓟 (s \ ⋃ (y : α) (_ : y ∈ i), {x | (x, y) ∈ d}) ≥ 𝓟 (s \ ⋃ (y : α) (_ : y ∈ j), {x | (x, y) ∈ d})

case refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
⊢ ∀ (i : Finset α), NeBot (𝓟 (s \ ⋃ (y : α) (_ : y ∈ i), {x | (x, y) ∈ d}))
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
⊢ NeBot f
refine' iInf_neBot_of_directed' (directed_of_sup _) _
case refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
t₁ t₂ : Finset α
h : t₁ ≤ t₂
⊢ 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t₁), {x | (x, y) ∈ d}) ≥ 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t₂), {x | (x, y) ∈ d})
case refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
⊢ ∀ ⦃i j : Finset α⦄,
    i ≤ j → 𝓟 (s \ ⋃ (y : α) (_ : y ∈ i), {x | (x, y) ∈ d}) ≥ 𝓟 (s \ ⋃ (y : α) (_ : y ∈ j), {x | (x, y) ∈ d})
intro t₁ t₂ h
no goals
case refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
t₁ t₂ : Finset α
h : t₁ ≤ t₂
⊢ 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t₁), {x | (x, y) ∈ d}) ≥ 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t₂), {x | (x, y) ∈ d})
exact principal_mono.2 (diff_subset_diff_right <| biUnion_subset_biUnion_left h)
case refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
t : Finset α
⊢ NeBot (𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}))
case refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
⊢ ∀ (i : Finset α), NeBot (𝓟 (s \ ⋃ (y : α) (_ : y ∈ i), {x | (x, y) ∈ d}))
intro t
no goals
case refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
t : Finset α
⊢ NeBot (𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}))
simpa [nonempty_diff] using hd_cover t t.finite_toSet
no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), Set.Finite t → ¬s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}
f : Filter α := ⨅ (t : Finset α), 𝓟 (s \ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d})
this : NeBot f
⊢ 𝓟 (s \ ⋃ (y : α) (_ : y ∈ ∅), {x | (x, y) ∈ d}) ≤ 𝓟 s
simp