no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.254383
ι✝ : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t : Set β
ι : Sort u_1
f : ι → Filter β
m : α → β
s : Set α
hs : s ∈ ⨆ (i : ι), comap m (f i)
⊢ ∀ (i : ι), ∃ t, t ∈ f i ∧ m ⁻¹' t ⊆ s
simpa only [mem_comap, exists_prop, mem_iSup] using mem_iSup.1 hs
α : Type u
β : Type v
γ : Type w
δ : Type ?u.254383
ι✝ : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
ι : Sort u_1
f : ι → Filter β
m : α → β
s : Set α
hs : s ∈ ⨆ (i : ι), comap m (f i)
this : ∀ (i : ι), ∃ t, t ∈ f i ∧ m ⁻¹' t ⊆ s
t : ι → Set β
ht : ∀ (x : ι), t x ∈ f x ∧ m ⁻¹' t x ⊆ s
⊢ ∀ (i : ι), m ⁻¹' t i ⊆ s
α : Type u
β : Type v
γ : Type w
δ : Type ?u.254383
ι✝ : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
ι : Sort u_1
f : ι → Filter β
m : α → β
s : Set α
hs : s ∈ ⨆ (i : ι), comap m (f i)
this : ∀ (i : ι), ∃ t, t ∈ f i ∧ m ⁻¹' t ⊆ s
t : ι → Set β
ht : ∀ (x : ι), t x ∈ f x ∧ m ⁻¹' t x ⊆ s
⊢ (m ⁻¹' ⋃ (i : ι), t i) ⊆ s
rw [preimage_iUnion, iUnion_subset_iff]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.254383
ι✝ : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
ι : Sort u_1
f : ι → Filter β
m : α → β
s : Set α
hs : s ∈ ⨆ (i : ι), comap m (f i)
this : ∀ (i : ι), ∃ t, t ∈ f i ∧ m ⁻¹' t ⊆ s
t : ι → Set β
ht : ∀ (x : ι), t x ∈ f x ∧ m ⁻¹' t x ⊆ s
⊢ ∀ (i : ι), m ⁻¹' t i ⊆ s
exact fun i => (ht i).2