preimage — Mathlib

English

For a finite subset s of β and a map f: α → β, the preimage Finset consists of all a in α with f(a) ∈ s.

Русский

Для конечного подмножества s ⊆ β и отображения f: α → β предобразом считается конечное множество всех a ∈ α таких, что f(a) ∈ s.

LaTeX

$$$$ \\mathrm{preimage}(s,f,hf) = \\{ a \\in \\alpha \\mid f(a) \\in s \\}. $$$$

Lean4

/-- Preimage of `s : Finset β` under a map `f` injective on `f ⁻¹' s` as a `Finset`. -/
noncomputable def preimage (s : Finset β) (f : α → β) (hf : Set.InjOn f (f ⁻¹' ↑s)) : Finset α :=
  (s.finite_toSet.preimage hf).toFinset

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