English
The image under f of the Finset of numerators equals the common denominator times the set s.
Русский
Образ f финитного множества числителей равен общему знаменателю, умноженному на множество s.
LaTeX
$$$f''\mathrm{finsetIntegerMultiple}(S,f,s) = \mathrm{commonDenomOfFinset}(S,f,s) \cdot (s : Set M')$$$
Lean4
theorem finsetIntegerMultiple_image [DecidableEq M] (s : Finset M') :
f '' finsetIntegerMultiple S f s = commonDenomOfFinset S f s • (s : Set M') :=
by
delta finsetIntegerMultiple commonDenom
rw [Finset.coe_image]
ext
constructor
· rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩
rw [map_integerMultiple]
exact Set.mem_image_of_mem _ x.prop
· rintro ⟨x, hx, rfl⟩
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple S f s id _⟩