α : Type u_2
ι : Type u_1
ι' : Type ?u.1728
inst✝² : DecidableEq ι
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : PairwiseDisjoint (↑s) f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ PairwiseDisjoint (g '' ↑s) f
α : Type u_2
ι : Type u_1
ι' : Type ?u.1728
inst✝² : DecidableEq ι
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : PairwiseDisjoint (↑s) f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ PairwiseDisjoint (↑(Finset.image g s)) f
rw [coe_image]
no goals
α : Type u_2
ι : Type u_1
ι' : Type ?u.1728
inst✝² : DecidableEq ι
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : PairwiseDisjoint (↑s) f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ PairwiseDisjoint (g '' ↑s) f
exact hs.image_of_le hf