compl_dom_subset_core — Mathlib

English

For any set s ⊆ β, any x not in the domain of f automatically lies in the core of s with respect to f. In other words, f.Domᶜ is contained in f.core(s).

Русский

Для любой множества s ⊆ β любой x, не принадлежащий области определения f, автоматически принадлежит ядру s относительно f. Другими словами, f.Domᶜ ⊆ f.core(s).

LaTeX

$$$$ x \notin \mathrm{Dom}(f) \implies x \in f.core(s). $$$$

Lean4

theorem compl_dom_subset_core (s : Set β) : f.Domᶜ ⊆ f.core s := fun x hx y fxy =>
  absurd ((mem_dom f x).mpr ⟨y, fxy⟩) hx

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