α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ i, y ∈ (f i).sets
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, (x ∈ ⋃ (i : ι), (f i).sets) → x ⊆ y → y ∈ ⋃ (i : ι), (f i).sets
simp only [mem_iUnion, exists_imp]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ i, y ∈ (f i).sets
exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, (x ∈ ⋃ (i : ι), (f i).sets) → (y ∈ ⋃ (i : ι), (f i).sets) → x ∩ y ∈ ⋃ (i : ι), (f i).sets
simp only [mem_iUnion, exists_imp]
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
⊢ ∃ i, x ∩ y ∈ (f i).sets
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets
intro x y a hx b hy
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
c : ι
ha : f a ≥ f c
hb : f b ≥ f c
⊢ ∃ i, x ∩ y ∈ (f i).sets
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
⊢ ∃ i, x ∩ y ∈ (f i).sets
rcases h a b with ⟨c, ha, hb⟩
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
c : ι
ha : f a ≥ f c
hb : f b ≥ f c
⊢ ∃ i, x ∩ y ∈ (f i).sets
exact ⟨c, inter_mem (ha hx) (hb hy)⟩
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.94306
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
ne : Nonempty ι
i : ι
u : Filter α :=
  { sets := ⋃ (i : ι), (f i).sets, univ_sets := (_ : univ ∈ ⋃ (i : ι), (f i).sets), sets_of_superset := ?m.94704,
    inter_sets := ?m.94705 }
this : u = iInf f
⊢ u.sets = ⋃ (i : ι), (f i).sets
simp only