core_res — Mathlib

English

The core of the restricted function equals the union of the complement of the domain and the preimage of t under f: (res f s).core t = sᶜ ∪ f⁻¹(t).

Русский

Ядро ограниченной функции равно объединению комплемента области определения и предобраза t по f: (res f s).core t = sᶜ ∪ f⁻¹(t).

LaTeX

$$$$ (\mathrm{res} f s).core(t) = s^{\mathrm{c}} \cup f^{-1}(t). $$$$

Lean4

theorem core_res (f : α → β) (s : Set α) (t : Set β) : (res f s).core t = sᶜ ∪ f ⁻¹' t :=
  by
  ext x
  rw [mem_core_res]
  by_cases h : x ∈ s <;> simp [h]

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