mem_map — Mathlib

English

For y ∈ L, y ∈ s.map f iff ∃ x ∈ s with f(x) = y.

Русский

Для y ∈ L верно: y ∈ s.map f тогда и только если существует x ∈ s, такое что f(x) = y.

LaTeX

$$$ y \in s.map f \quad\Leftrightarrow\quad \exists x\in s, f(x) = y $$$

Lean4

@[simp]
theorem mem_map {f : K →+* L} {s : Subfield K} {y : L} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y :=
  by
  unfold map
  simp only [mem_mk, Subring.mem_map, mem_toSubring]

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