subset_upperPolar_iff_subset_lowerPolar

Mathlib.Order.Concept

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

← MathLib Explorer

English

There is a duality between t ⊆ upperPolar r s and s ⊆ lowerPolar r t.

Русский

Существует двойственность между t ⊆ upperPolar r s и s ⊆ lowerPolar r t.

LaTeX

$$$t \subseteq \upperPolar\,r\,s \iff s \subseteq \lowerPolar\,r\,t$$$

Lean4

theorem subset_upperPolar_iff_subset_lowerPolar : t ⊆ upperPolar r s ↔ s ⊆ lowerPolar r t :=
  ⟨fun h _ ha _ hb => h hb ha, fun h _ hb _ ha => h ha hb⟩

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

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

Разделы

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

Аффилиация

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