mem_of_star_mem

Mathlib.Algebra.Star.Basic

URI: https://scilib.ai/kg/mathlib#mem_of_star_mem

← MathLib Explorer

English

If star r ∈ s, then r ∈ s.

Русский

Если star r ∈ s, то r ∈ s.

LaTeX

$$$$ \star r \in s \Rightarrow r \in s. $$$$

Lean4

@[aesop 5% (rule_sets := [SetLike!])]
theorem mem_of_star_mem {S R : Type*} [InvolutiveStar R] [SetLike S R] [StarMemClass S R] {s : S} {r : R}
    (hr : star r ∈ s) : r ∈ s := by rw [← star_star r]; exact star_mem hr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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