nonempty_star — Mathlib

English

If α has an involutive star, then for any set s, s⋆ is nonempty iff s is nonempty.

Русский

Если α имеет инволютивную звезду, то для любого множества s верно: s⋆ не пусто тогда и только тогда, когда s не пусто.

LaTeX

$$$\\operatorname{Nonempty}(s^{\\star}) \\iff \\operatorname{Nonempty}(s).$$$

Lean4

@[simp]
theorem nonempty_star [InvolutiveStar α] {s : Set α} : s⋆.Nonempty ↔ s.Nonempty :=
  star_involutive.surjective.nonempty_preimage

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