α : Type u
β : Type v
γ : Type w
δ : Type ?u.280594
ι✝ : Sort x
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}
ne : ∃ i, p i
this : Nonempty { a // p a }
⊢ map m (⨅ (i : ι) (_ : p i), f i) = ⨅ (i : ι) (_ : p i), map m (f i)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.280594
ι✝ : Sort x
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}
ne : ∃ i, p i
⊢ map m (⨅ (i : ι) (_ : p i), f i) = ⨅ (i : ι) (_ : p i), map m (f i)
haveI := nonempty_subtype.2 ne
α : Type u
β : Type v
γ : Type w
δ : Type ?u.280594
ι✝ : Sort x
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}
ne : ∃ i, p i
this : Nonempty { a // p a }
⊢ map m (⨅ (x : { i // p i }), f ↑x) = ⨅ (x : { i // p i }), map m (f ↑x)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.280594
ι✝ : Sort x
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}
ne : ∃ i, p i
this : Nonempty { a // p a }
⊢ map m (⨅ (i : ι) (_ : p i), f i) = ⨅ (i : ι) (_ : p i), map m (f i)
simp only [iInf_subtype']
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.280594
ι✝ : Sort x
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}
ne : ∃ i, p i
this : Nonempty { a // p a }
⊢ map m (⨅ (x : { i // p i }), f ↑x) = ⨅ (x : { i // p i }), map m (f ↑x)
exact map_iInf_eq h.directed_val