valueGroup_eq_range — Mathlib

English

The image of valueGroup f under Units.val equals range f without zero: Units.val '' (valueGroup f) = range f \ {0}.

Русский

Образ valueGroup f под Units.val равен range f без нуля: Units.val '' (valueGroup f) = range f \ {0}.

LaTeX

$$Units.val '' (valueGroup f) = (range f \ {0})$$

Lean4

theorem valueGroup_eq_range : Units.val '' (valueGroup f) = (range f \ {0}) :=
  by
  ext x
  simp only [mem_diff, mem_range, mem_singleton_iff, ← valueMonoid_eq_valueGroup' f, mem_image, SetLike.mem_coe,
    mem_valueMonoid_iff, mem_preimage, mem_range]
  constructor
  · rintro ⟨y, hy, rfl⟩
    simp only [Units.ne_zero, not_false_eq_true, and_true, hy]
  · rintro ⟨⟨y, hy⟩, hx₀⟩
    refine ⟨Units.mk0 x hx₀, ?_, rfl⟩
    simpa [Units.val_mk0, mem_range] using ⟨y, hy⟩

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