instTrivialStar — Mathlib

English

If the star operation is trivial on α, then the induced star operation on subsets of α is also trivial; every subset is fixed by the star operation on sets.

Русский

Если операция звезды на α тривиальна, то соответствующая операция звезды над подмножествами α тоже тривиальна; каждое множество фиксируется операцией звезды.

LaTeX

$$$\\\\forall s \\\\subseteq\\\\alpha, \\, s^{\\\\star} = s.$$$

Lean4

@[simp]
instance [Star α] [TrivialStar α] : TrivialStar (Set α) where
  star_trivial
    s := by
    rw [← star_preimage]
    ext1
    simp [star_trivial]

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