pi_univ_bot

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.pi_univ_bot

English

The right bottom product is bottom: L.prod ⊥ = ⊥.

Русский

Произведение с правым нулём равно нулю: L.prod ⊥ = ⊥.

LaTeX

$$L.prod (\\bot : Sublattice β) = ⊥$$

Lean4

theorem pi_univ_bot [Nonempty κ] : (pi univ fun _ ↦ ⊥ : Sublattice (∀ i, π i)) = ⊥ := by simp

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

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

Разделы

Аффилиация

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