star_mem_star

Mathlib.Algebra.Star.Pointwise

URI: https://scilib.ai/kg/mathlib#Set.star_mem_star

English

For any a, a⋆ ∈ s⋆ iff a ∈ s.

Русский

Для любого a, a⋆ ∈ s⋆ тогда и только тогда, когда a ∈ s.

LaTeX

$$$a^{\\star} \\in s^{\\star} \\iff a \\in s.$$$

Lean4

theorem star_mem_star [InvolutiveStar α] : a⋆ ∈ s⋆ ↔ a ∈ s := by simp only [mem_star, star_star]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru