finsetIntegerMultiple_image — Mathlib

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 _⟩

Похожие утверждения