inv

Mathlib.Algebra.Order.UpperLower

URI: https://scilib.ai/kg/mathlib#IsLowerSet.inv

English

If hs: IsLowerSet s, then IsUpperSet s⁻¹.

Русский

Если s — нижнее множество, то s⁻¹ — верхнее множество.

LaTeX

$$$IsLowerSet(s) \rightarrow IsUpperSet(s^{-1})$$$

Lean4

@[to_additive]
theorem inv (hs : IsLowerSet s) : IsUpperSet s⁻¹ := fun _ _ h ↦ hs <| inv_le_inv' h

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

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

Разделы

Аффилиация

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