mem_idealRange_iff — Mathlib

English

Characterization of idealRange: membership in idealRange is equivalent to existence of a preimage.

Русский

Характеризация idealRange: принадлежность эквивалентна существованию предобраза.

LaTeX

$$$f.IsIdealMorphism \\Rightarrow (\\forall y, y \\in \\mathrm{idealRange}(f) \\iff \\exists x, f(x)=y)$$$

Lean4

@[simp]
theorem mem_idealRange_iff (h : IsIdealMorphism f) {y : L'} : y ∈ idealRange f ↔ ∃ x : L, f x = y :=
  by
  rw [f.isIdealMorphism_def] at h
  rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.coe_range, Set.mem_range]

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