dualAnnihilator_eq_top_iff — Mathlib

English

Dually, W.dualAnnihilator = ⊤ iff W = ⊥ under appropriate projectivity hypotheses.

Русский

Соответствующим образом, W.dualAnnihilator = ⊤ эквивалентно W = ⊥ при подходящих предположениях проективности.

LaTeX

$$W.dualAnnihilator = ⊤ ↔ W = ⊥$$

Lean4

@[simp]
theorem dualAnnihilator_eq_top_iff {W : Submodule R M} [Projective R M] : W.dualAnnihilator = ⊤ ↔ W = ⊥ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dualAnnihilator_bot⟩
  refine W.eq_bot_iff.mpr fun v hv ↦ (forall_dual_apply_eq_zero_iff R v).mp fun f ↦ ?_
  refine (mem_dualAnnihilator f).mp ?_ v hv
  simp [h]

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