direction_eq_top_iff_of_nonempty — Mathlib

English

For a nonempty subspace s, s equals ⊤ if and only if its direction is ⊤.

Русский

Для непустого подпро пространства s верно: s = ⊤ тогда и только тогда, когда direction(s) = ⊤.

LaTeX

$$$ (s : \mathrm{Set} P).Nonempty \Rightarrow (s.direction = \top \iff s = \top)$$$

Lean4

/-- A nonempty affine subspace is `⊤` if and only if its direction is `⊤`. -/
@[simp]
theorem direction_eq_top_iff_of_nonempty {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    s.direction = ⊤ ↔ s = ⊤ := by
  constructor
  · intro hd
    rw [← direction_top k V P] at hd
    refine ext_of_direction_eq hd ?_
    simp [h]
  · rintro rfl
    simp

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