mem_preimage — Mathlib

English

An element x belongs to the preimage of s under f if and only if f(x) belongs to s.

Русский

Элемент x принадлежит предобразу s под f тогда и только тогда, когда f(x) принадлежит s.

LaTeX

$$$$ x \\in \\mathrm{preimage}(s,f,hf) \\iff f(x) \\in s. $$$$

Lean4

@[simp]
theorem mem_preimage {f : α → β} {s : Finset β} {hf : Set.InjOn f (f ⁻¹' ↑s)} {x : α} : x ∈ preimage s f hf ↔ f x ∈ s :=
  Set.Finite.mem_toFinset _

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