mapsTo_image_iff — Mathlib

English

MapsTo f (g''s) t is equivalent to MapsTo (f∘g) s t.

Русский

MapsTo f (g''s) t эквивалентно MapsTo (f∘g) s t.

LaTeX

$$$\\\\MapsTo f (\\\\mathrm{image}\_{\ } g\, s) t \\\\leftrightarrow \\\\MapsTo (f \\\\circ \\\\ g) s t$$$

Lean4

@[simp]
theorem mapsTo_image_iff {f : α → β} {g : γ → α} {s : Set γ} {t : Set β} : MapsTo f (g '' s) t ↔ MapsTo (f ∘ g) s t :=
  ⟨fun h c hc => h ⟨c, hc, rfl⟩, fun h _ ⟨_, hc⟩ => hc.2 ▸ h hc.1⟩

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