kernImage — Mathlib

English

The kernImage of f with respect to s is the set of y such that every x with f(x) = y belongs to s.

Русский

KernImage f s — множество y such that для всех x с f(x) = y следует x ∈ s.

LaTeX

$$$y \\in \\operatorname{kernImage}(f,s) \\iff \\forall x\\ \\bigl(f(x)=y \\Rightarrow x \\in s\\bigr)$$$

Lean4

/-- `kernImage f s` is the set of `y` such that `f ⁻¹ y ⊆ s`. -/
def kernImage (f : α → β) (s : Set α) : Set β :=
  {y | ∀ ⦃x⦄, f x = y → x ∈ s}

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