mem_range — Mathlib

English

x ∈ range f iff x ∈ Set.range f.

Русский

x принадлежит диапазону f тогда как x принадлежит множеству Set.range f.

LaTeX

$$$x \\in \\mathrm{range}\\ f \\iff x \\in \\mathrm{Set.range}\\ f$$$

Lean4

@[simp]
theorem mem_range {α} [Small.{u} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}} : x ∈ range f ↔ x ∈ Set.range f :=
  Quotient.inductionOn x fun y => by
    constructor
    · rintro ⟨z, hz⟩
      exact ⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩
    · rintro ⟨z, hz⟩
      use equivShrink α z
      simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)

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