unop_mem_unop

Mathlib.Data.Set.Opposite

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

English

Let s be a set of αᵒᵖ and a ∈ αᵒᵖ. Then unop a ∈ s.unop iff a ∈ s.

Русский

Пусть s — множество в αᵒᵖ и a ∈ αᵒᵖ. Тогда unop a ∈ s.unop ⇔ a ∈ s.

LaTeX

$$$\operatorname{unop} a \in s.unop \iff a \in s$$$

Lean4

@[simp 1100]
theorem unop_mem_unop {s : Set αᵒᵖ} {a : αᵒᵖ} : unop a ∈ s.unop ↔ a ∈ s := by rfl

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

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

Разделы

Аффилиация

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