α : Type u
β : Type v
γ : Type w
δ : Type ?u.114761
ι : Sort x
f g : Filter α
s✝ t✝ s t : Set α
⊢ ∃ t₁, t₁ ∈ 𝓟 s ∧ ∃ t₂, t₂ ∈ 𝓟 t ∧ s ∩ t = t₁ ∩ t₂
α : Type u
β : Type v
γ : Type w
δ : Type ?u.114761
ι : Sort x
f g : Filter α
s✝ t✝ s t : Set α
⊢ 𝓟 s ⊓ 𝓟 t ≤ 𝓟 (s ∩ t)
simp only [le_principal_iff, mem_inf_iff]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.114761
ι : Sort x
f g : Filter α
s✝ t✝ s t : Set α
⊢ ∃ t₁, t₁ ∈ 𝓟 s ∧ ∃ t₂, t₂ ∈ 𝓟 t ∧ s ∩ t = t₁ ∩ t₂
exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.114761
ι : Sort x
f g : Filter α
s✝ t✝ s t : Set α
⊢ 𝓟 (s ∩ t) ≤ 𝓟 s ⊓ 𝓟 t
simp [le_inf_iff, inter_subset_left, inter_subset_right]