case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) ↔ G ∈ Compactum.basic A ∩ Compactum.basic B
X : Compactum
A B : Set X.A
⊢ Compactum.basic (A ∩ B) = Compactum.basic A ∩ Compactum.basic B
ext G
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) → G ∈ Compactum.basic A ∩ Compactum.basic B

case h.mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B → G ∈ Compactum.basic (A ∩ B)
case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) ↔ G ∈ Compactum.basic A ∩ Compactum.basic B
constructor
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) → G ∈ Compactum.basic A ∩ Compactum.basic B
intro hG
case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ A

case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ B
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B
constructor <;> filter_upwards [hG]with _
no goals
case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ A

case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ B
exacts [And.left, And.right]
case h.mpr.intro
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h1 : G ∈ Compactum.basic A
h2 : G ∈ Compactum.basic B
⊢ G ∈ Compactum.basic (A ∩ B)
case h.mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B → G ∈ Compactum.basic (A ∩ B)
rintro ⟨h1, h2⟩
no goals
case h.mpr.intro
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h1 : G ∈ Compactum.basic A
h2 : G ∈ Compactum.basic B
⊢ G ∈ Compactum.basic (A ∩ B)
exact inter_mem h1 h2