star_mem_iff — Mathlib

English

For a star-closed set S in R, star x ∈ S iff x ∈ S.

Русский

Для множества S, замкнутого относительно операции звезды, имеет место star x ∈ S ↔ x ∈ S.

LaTeX

$$$$ \star x \in s \iff x \in s. $$$$

Lean4

theorem star_mem_iff {S : Type*} [SetLike S R] [InvolutiveStar R] [StarMemClass S R] {s : S} {x : R} :
    star x ∈ s ↔ x ∈ s :=
  ⟨fun h => star_star x ▸ star_mem h, fun h => star_mem h⟩

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