case inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110881
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x x_1 => x ≥ x_1) f
hb : ∀ (i : ι), NeBot (f i)
h✝ : IsEmpty ι
⊢ NeBot (iInf f)

case inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110881
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x x_1 => x ≥ x_1) f
hb : ∀ (i : ι), NeBot (f i)
h✝ : Nonempty ι
⊢ NeBot (iInf f)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110881
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x x_1 => x ≥ x_1) f
hb : ∀ (i : ι), NeBot (f i)
⊢ NeBot (iInf f)
cases isEmpty_or_nonempty ι
case inl.ne'
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110881
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x x_1 => x ≥ x_1) f
hb : ∀ (i : ι), NeBot (f i)
h✝ : IsEmpty ι
⊢ iInf f ≠ ⊥
case inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110881
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x x_1 => x ≥ x_1) f
hb : ∀ (i : ι), NeBot (f i)
h✝ : IsEmpty ι
⊢ NeBot (iInf f)
constructor
no goals
case inl.ne'
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110881
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x x_1 => x ≥ x_1) f
hb : ∀ (i : ι), NeBot (f i)
h✝ : IsEmpty ι
⊢ iInf f ≠ ⊥
simp [iInf_of_empty f, top_ne_bot]
no goals
case inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110881
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x x_1 => x ≥ x_1) f
hb : ∀ (i : ι), NeBot (f i)
h✝ : Nonempty ι
⊢ NeBot (iInf f)
exact iInf_neBot_of_directed' hd hb