mapsTo_singleton

Mathlib.Data.Set.Function

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

English

MapsTo f {x} t holds if and only if f(x) ∈ t.

Русский

MapsTo f {x} t эквивалентно f(x) ∈ t.

LaTeX

$$$ MapsTo\\ f\\ {x}\\ t \\iff f\\,x \\in t $$$

Lean4

@[simp]
theorem mapsTo_singleton {x : α} : MapsTo f { x } t ↔ f x ∈ t :=
  singleton_subset_iff

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

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

Разделы

Аффилиация

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