α : Type u_1
β : Type u_2
γ : Type ?u.64418
ι : Sort ?u.64421
ι' : Sort ?u.64424
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S
ne : Set.Nonempty S
t : Set α
⊢ DirectedOn ((fun i => 𝓟 (s i)) ⁻¹'o fun x x_1 => x ≥ x_1) S
α : Type u_1
β : Type u_2
γ : Type ?u.64418
ι : Sort ?u.64421
ι' : Sort ?u.64424
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S
ne : Set.Nonempty S
t : Set α
⊢ (t ∈ ⨅ (i : β) (_ : i ∈ S), 𝓟 (s i)) ↔ ∃ i, i ∈ S ∧ s i ⊆ t
refine' mem_biInf_of_directed _ ne
α : Type u_1
β : Type u_2
γ : Type ?u.64418
ι : Sort ?u.64421
ι' : Sort ?u.64424
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : β → Set α
S : Set β
h : Directed (fun x x_1 => x ≥ x_1) (s ∘ Subtype.val)
ne : Set.Nonempty S
t : Set α
⊢ Directed (fun x x_1 => x ≥ x_1) ((fun i => 𝓟 (s i)) ∘ Subtype.val)
α : Type u_1
β : Type u_2
γ : Type ?u.64418
ι : Sort ?u.64421
ι' : Sort ?u.64424
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S
ne : Set.Nonempty S
t : Set α
⊢ DirectedOn ((fun i => 𝓟 (s i)) ⁻¹'o fun x x_1 => x ≥ x_1) S
rw [directedOn_iff_directed, ← directed_comp] at h ⊢
α : Type u_1
β : Type u_2
γ : Type ?u.64418
ι : Sort ?u.64421
ι' : Sort ?u.64424
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : β → Set α
S : Set β
h : Directed (fun x x_1 => x ≥ x_1) (s ∘ Subtype.val)
ne : Set.Nonempty S
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y
α : Type u_1
β : Type u_2
γ : Type ?u.64418
ι : Sort ?u.64421
ι' : Sort ?u.64424
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : β → Set α
S : Set β
h : Directed (fun x x_1 => x ≥ x_1) (s ∘ Subtype.val)
ne : Set.Nonempty S
t : Set α
⊢ Directed (fun x x_1 => x ≥ x_1) ((fun i => 𝓟 (s i)) ∘ Subtype.val)
refine' h.mono_comp _
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.64418
ι : Sort ?u.64421
ι' : Sort ?u.64424
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : β → Set α
S : Set β
h : Directed (fun x x_1 => x ≥ x_1) (s ∘ Subtype.val)
ne : Set.Nonempty S
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y
exact fun _ _ => principal_mono.2