Theorems · Theorem · geometry

AffineSubspace.lt_iff_le_and_exists

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

A subspace is less than another if and only if it is less than or equal to the second subspace and there is a point only in the second.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsor