eq_restrict_iff — Mathlib

English

A function f on α equals the restriction of g to s if and only if, for all a ∈ s, f(a) = g(a).

Русский

Функция f на α равна ограничению g на s тогда и только тогда, когда для всех a ∈ s выполняется f(a) = g(a).

LaTeX

$$$f = \operatorname{restrict}(s,g) \iff \forall a\in s, f(a) = g(a)$$$

Lean4

theorem eq_restrict_iff {s : Set α} {f : ∀ a : s, π a} {g : ∀ a, π a} :
    f = restrict s g ↔ ∀ (a) (ha : a ∈ s), f ⟨a, ha⟩ = g a :=
  funext_iff.trans Subtype.forall

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