codisjoint_mk_iff — Mathlib

English

Codisjoint of ⟨p, hp⟩ and ⟨q, hq⟩ in f.invtSubmodule iff codisjoint of p and q.

Русский

Кодисjoint для представлений в f.invtSubmodule эквивалентен кодисjoint-у самих подмодулей.

LaTeX

$$$\text{Codisjoint}(\langle p, hp\rangle, \langle q, hq\rangle) \iff \text{Codisjoint}(p, q)$$$

Lean4

@[simp]
protected theorem codisjoint_mk_iff {p q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) :
    Codisjoint (α := f.invtSubmodule) ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint p q := by
  rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk, Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]

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