Theorems · Theorem · linear algebra

Submodule.sup_inf_assoc_of_le_of_neg_le

∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Submodule R M}
  (t : Submodule R M) {p : Submodule R M}, s ≤ p → -s ≤ p → (s ⊔ t) ⊓ p = s ⊔ t ⊓ p

Defined in

Mathlib.LinearAlgebra.Span.Basic

Cited by

2 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommGroupModule