mem_map

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.mem_map

English

An element y lies in the image of S under f if and only if there exists x in S with f(x) = y.

Русский

Элемент y принадлежит образу S под действием f iff существует x ∈ S such that f(x) = y.

LaTeX

$$y \in \operatorname{map}(f,S) \iff \exists x \in S, f(x) = y.$$

Lean4

@[simp]
theorem mem_map {S : NonUnitalStarSubalgebra R A} {f : F} {y : B} : y ∈ map f S ↔ ∃ x ∈ S, f x = y :=
  NonUnitalSubalgebra.mem_map

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

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

Разделы

Аффилиация

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