parallel_bot_iff_eq_bot — Mathlib

English

A subspace S is parallel to the bottom (⊥) iff S is the bottom itself: S ∥ ⊥ iff S = ⊥.

Русский

Подпространство S параллельно нулю тогда и только тогда, когда S равно нулю: S ∥ ⊥ ⇔ S = ⊥.

LaTeX

$$$ S \\parallel \\bot \\,\\Longrightarrow\\, S = \\bot $ and conversely $ S = \\bot \\Rightarrow S \\parallel \\bot $$$

Lean4

@[simp]
theorem parallel_bot_iff_eq_bot {s : AffineSubspace k P} : s ∥ ⊥ ↔ s = ⊥ :=
  by
  refine ⟨fun h => ?_, fun h => h ▸ Parallel.refl _⟩
  rcases h with ⟨v, h⟩
  rwa [eq_comm, map_eq_bot_iff] at h

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