closure_mono — Mathlib

English

If g is closable and f ≤ g, then f.closure ≤ g.closure.

Русский

Если g замыкаемо и f ≤ g, то f.closure ≤ g.closure.

LaTeX

$$$g \IsClosable \land f \le g \Rightarrow f.closure \le g.closure$$$

Lean4

theorem closure_mono {f g : E →ₗ.[R] F} (hg : g.IsClosable) (h : f ≤ g) : f.closure ≤ g.closure :=
  by
  refine le_of_le_graph ?_
  rw [← (hg.leIsClosable h).graph_closure_eq_closure_graph]
  rw [← hg.graph_closure_eq_closure_graph]
  exact Submodule.topologicalClosure_mono (le_graph_of_le h)

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