InjOn — Mathlib

English

Let f: α → β and s ⊆ α. The restriction of f to s is injective; i.e., for any x1, x2 ∈ s, f(x1) = f(x2) implies x1 = x2.

Русский

Пусть f: α → β и s ⊆ α. Ограничение f на s инъективно; то есть для любых x1, x2 ∈ s выполняется f(x1) = f(x2) ⇒ x1 = x2.

LaTeX

$$$\operatorname{InjOn}(f,s) \iff \forall x_1 \in s \; \forall x_2 \in s \; (f(x_1) = f(x_2) \Rightarrow x_1 = x_2)$$$

Lean4

/-- `f` is injective on `s` if the restriction of `f` to `s` is injective. -/
def InjOn (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂

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