mapsTo_range_iff

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.mapsTo_range_iff

English

MapsTo f (range g) t iff ∀ i, f (g i) ∈ t.

Русский

MapsTo f (range g) t эквивалентно ∀ i, f (g i) ∈ t.

LaTeX

$$$\\\\MapsTo f (\\\\mathrm{range} \\\\! g) t \\\\leftrightarrow \\\\forall i, f (g i) \\in t$$$

Lean4

@[simp]
theorem mapsTo_range_iff {g : ι → α} : MapsTo f (range g) t ↔ ∀ i, f (g i) ∈ t :=
  forall_mem_range

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru