LeftInvOn — Mathlib

English

Let g: β → α, f: α → β, s ⊆ α. Then g is a left inverse to f on s if g(f(x)) = x for all x ∈ s.

Русский

Пусть g: β → α, f: α → β, s ⊆ α. Тогда g является левым обратным к f на s, если для всех x ∈ s выполняется g(f(x)) = x.

LaTeX

$$$\mathrm{LeftInvOn}(g,f,s) \iff \forall x\,(x \in s \to g(f(x)) = x)$$$

Lean4

/-- `g` is a left inverse to `f` on `s` means that `g (f x) = x` for all `x ∈ s`. -/
def LeftInvOn (g : β → α) (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃x⦄, x ∈ s → g (f x) = x

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