left_top_iff — Mathlib

English

A top submodule on the N-side is determined by the IsPerfectCompl condition with the top submodule; specifically, p.IsPerfectCompl ⊤ V iff V = ⊤.

Русский

Условие IsPerfectCompl для верхнего подмодуля слева задаёт топ-подмодуль; p.IsPerfectCompl ⊤ V эквивалентно V = ⊤.

LaTeX

$$$p.IsPerfectCompl \\top V \\iff V = \\top$.$$

Lean4

@[simp]
theorem left_top_iff : p.IsPerfectCompl ⊤ V ↔ V = ⊤ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · exact eq_top_of_isCompl_bot <| by simpa using h.isCompl_right
  · rw [h]
    exact
      { isCompl_left := by simpa using isCompl_top_bot
        isCompl_right := by simpa using isCompl_top_bot }

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