instIsSimpleOrderOfSubsingleton — Mathlib

English

If P is a subsingleton, then the order on affine subspaces is simple: every subspace is either ⊥ or ⊤.

Русский

Если P — одиночное множество, то порядок над аффинными подпро пространство упрощён: любое подпространство равно ⊥ или ⊤.

LaTeX

$$$P$ subsingleton \Rightarrow \forall Q,\ Q = \bot \lor Q = \top$$$

Lean4

instance [Subsingleton P] : IsSimpleOrder (AffineSubspace k P) where
  eq_bot_or_eq_top
    (s : AffineSubspace k P) := by
    rw [← coe_eq_bot_iff, ← coe_eq_univ_iff]
    rcases (s : Set P).eq_empty_or_nonempty with h | h
    · exact .inl h
    · exact .inr h.eq_univ

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