op_mem_op

Mathlib.Data.Set.Opposite

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

English

op(a) ∈ s.op iff a ∈ s.

Русский

op(a) ∈ s.op эквивалентно a ∈ s.

LaTeX

$$$$ \\operatorname{op}(a) \\in s^{\\mathrm{op}} \\iff a \\in s $$$$

Lean4

@[simp 1100]
theorem op_mem_op {s : Set α} {a : α} : op a ∈ s.op ↔ a ∈ s := by rfl

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

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

Разделы

Аффилиация

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