star_mem_star_iff

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.star_mem_star_iff

English

Another equivalent formulation: star x ∈ star S iff x ∈ S.

Русский

Еще одна эквивалентная формулировка: star x ∈ star S ⇔ x ∈ S.

LaTeX

$$$star\\ x \\in star S \\iff x \\in S$$$

Lean4

theorem star_mem_star_iff (S : Subalgebra R A) (x : A) : star x ∈ star S ↔ x ∈ S := by simp

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

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

Разделы

Аффилиация

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