supPrime_iff_supIrred

Mathlib.Order.Irreducible

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

← MathLib Explorer

English

In a distributive lattice, SupPrime is equivalent to SupIrred.

Русский

В распределительной решётке SupPrime эквивалентен SupIrred.

LaTeX

$$$\SupPrime a \iff \SupIrred a$$$

Lean4

@[simp]
theorem supPrime_iff_supIrred : SupPrime a ↔ SupIrred a :=
  ⟨SupPrime.supIrred, And.imp_right fun h b c => by simp_rw [← inf_eq_left, inf_sup_left]; exact @h _ _⟩

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

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

Разделы

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

Аффилиация

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