mem_range

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.mem_range

← MathLib Explorer

English

For φ: A → B, y ∈ (range φ) iff there exists x ∈ A with φ(x) = y.

Русский

Для φ: A → B верно: y ∈ образ φ тогда, когда существует x ∈ A с φ(x) = y.

LaTeX

$$$y \\in \\mathrm{range}(\\phi) \\iff \\exists x:\\!A, \\phi(x) = y$$$

Lean4

@[simp]
theorem mem_range (φ : F) {y : B} : y ∈ (NonUnitalAlgHom.range φ : NonUnitalSubalgebra R B) ↔ ∃ x : A, φ x = y :=
  NonUnitalRingHom.mem_srange

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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