comap_incl_eq_bot — Mathlib

English

A dual criterion: if the comap of inclusion is bottom, then the intersection of N and N₂ is bottom.

Русский

Двойной критерий: если comap по включению — ноль, то пересечение N и N₂ равно нулю.

LaTeX

$$$ N_2.comap N.incl = \bot \iff N \cap N_2 = \bot $$$

Lean4

theorem comap_incl_eq_bot : N₂.comap N.incl = ⊥ ↔ N ⊓ N₂ = ⊥ :=
  by
  simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, bot_toSubmodule, inf_toSubmodule]
  rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]

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