spanPoints_nonempty — Mathlib

English

The spanPoints of a set s is nonempty if and only if s is nonempty.

Русский

spanPoints k s непустuy если и только если s непусто.

LaTeX

$$$spanPoints(k,s).Nonempty \\iff s.Nonempty$$$

Lean4

/-- The `spanPoints` of a set is nonempty if and only if that set is. -/
@[simp]
theorem spanPoints_nonempty (s : Set P) : (spanPoints k s).Nonempty ↔ s.Nonempty :=
  by
  constructor
  · contrapose
    rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]
    intro h
    simp [h, spanPoints]
  · exact fun h => h.mono (subset_spanPoints _ _)

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