mem_frange — Mathlib

English

An element y belongs to frange(f) iff y ≠ 0 and there exists x with f(x) = y.

Русский

Членство y в frange(f) эквивалентно y ≠ 0 и существует x с f(x) = y.

LaTeX

$$$$ y \\in f.frange \\iff y \\neq 0 \\land \\exists x, f x = y. $$$$

Lean4

theorem mem_frange {f : α →₀ M} {y : M} : y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y :=
  by
  rw [frange, @Finset.mem_image _ _ (Classical.decEq _) _ f.support]
  exact
    ⟨fun ⟨x, hx1, hx2⟩ => ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩, fun ⟨hy, x, hx⟩ =>
      ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩

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