mem_res — Mathlib

English

For f : α → β and s ⊆ α, for all a ∈ α and b ∈ β, b ∈ res f s a iff a ∈ s ∧ f a = b.

Русский

Для любой функции f: α → β и подмножества s ⊆ α, для всех a ∈ α и b ∈ β, b ∈ res f s a тогда и только тогда, когда a ∈ s и f a = b.

LaTeX

$$$b \\in \\mathrm{res}(f,s)(a) \\iff a \\in s \\wedge f(a) = b$$$

Lean4

theorem mem_res (f : α → β) (s : Set α) (a : α) (b : β) : b ∈ res f s a ↔ a ∈ s ∧ f a = b := by simp [res, @eq_comm _ b]

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