closureHasCore — Mathlib

English

The closure f.closure has f.domain as a core.

Русский

Замыкание f имеет домен f как ядро.

LaTeX

$$$f.closure.HasCore f.domain$$$

Lean4

/-- For every unbounded operator `f` the submodule `f.domain` is a core of its closure.

Note that we don't require that `f` is closable, due to the definition of the closure. -/
theorem closureHasCore (f : E →ₗ.[R] F) : f.closure.HasCore f.domain :=
  by
  refine ⟨f.le_closure.1, ?_⟩
  congr
  ext x h1 h2
  · simp only [domRestrict_domain, Submodule.mem_inf, and_iff_left_iff_imp]
    intro hx
    exact f.le_closure.1 hx
  let z : f.closure.domain := ⟨x, f.le_closure.1 h2⟩
  have hyz : x = z := rfl
  rw [f.le_closure.2 hyz]
  exact domRestrict_apply hyz

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