α : Type u
β : Type v
γ : Type ?u.19128
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ comap f inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) (_ : Injective (n ∘ m))
⊢ n '' range m ∈ f
α : Type u
β : Type v
γ : Type ?u.19128
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ comap f inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) (_ : Injective (n ∘ m))
⊢ range (n ∘ m) ∈ f
rw [range_comp]
no goals
α : Type u
β : Type v
γ : Type ?u.19128
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ comap f inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) (_ : Injective (n ∘ m))
⊢ n '' range m ∈ f
exact image_mem_of_mem_comap large₀ large₁