down_up

Mathlib.Data.Set.Semiring

URI: https://scilib.ai/kg/mathlib#SetSemiring.down_up

English

For every s in SetSemiring α, applying down then up yields s; i.e., (s.down).up = s.

Русский

Для любого s ∈ SetSemiring α выполняется (s.down).up = s.

LaTeX

$$(s.down).up = s$$

Lean4

@[simp]
protected theorem down_up (s : Set α) : s.up.down = s :=
  rfl

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

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

Разделы

Аффилиация

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