X : Type ?u.16388
α : Type u_1
α' : Type ?u.16394
β : Type u_2
γ : Type u_3
δ : Type u_4
M : Type ?u.16406
E : Type ?u.16409
R : Type ?u.16412
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x => m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1
X : Type ?u.16388
α : Type u_1
α' : Type ?u.16394
β : Type u_2
γ : Type u_3
δ : Type u_4
M : Type ?u.16406
E : Type ?u.16409
R : Type ?u.16412
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
hf₂ : HasCompactMulSupport f₂
hm : m 1 1 = 1
⊢ HasCompactMulSupport fun x => m (f x) (f₂ x)
rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂⊢
no goals
X : Type ?u.16388
α : Type u_1
α' : Type ?u.16394
β : Type u_2
γ : Type u_3
δ : Type u_4
M : Type ?u.16406
E : Type ?u.16409
R : Type ?u.16412
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x => m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1
filter_upwards [hf, hf₂]using fun x hx hx₂ => by simp_rw [hx, hx₂, Pi.one_apply, hm]
no goals
X : Type ?u.16388
α : Type u_1
α' : Type ?u.16394
β : Type u_2
γ : Type u_3
δ : Type u_4
M : Type ?u.16406
E : Type ?u.16409
R : Type ?u.16412
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x✝ : α
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = OfNat.ofNat 1 x
hx₂ : f₂ x = OfNat.ofNat 1 x
⊢ m (f x) (f₂ x) = OfNat.ofNat 1 x
simp_rw [hx, hx₂, Pi.one_apply, hm]