eq_univ_of_subsingleton_span_eq_top

English

If a subset s is Subsingleton and its affine span is the top, then s equals the whole space univ.

Русский

Если s — Subsingleton и affineSpan(k,s) = top, то s = univ.

LaTeX

$$$ s = (univ : Set P) $$$

Lean4

theorem eq_univ_of_subsingleton_span_eq_top {s : Set P} (h₁ : s.Subsingleton) (h₂ : affineSpan k s = ⊤) :
    s = (univ : Set P) :=
  by
  obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
  have : s = { p } := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
  rw [this, eq_comm, ← subsingleton_iff_singleton (mem_univ p), subsingleton_univ_iff]
  exact subsingleton_of_subsingleton_span_eq_top h₁ h₂

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