pi_univ_eq_bot

Mathlib.Order.Sublattice

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

English

Under nonempty α, nonempty β, L.prod M = ⊤ iff L = ⊤ and M = ⊤.

Русский

При непустых α, β, L.prod M = ⊤ тогда и только тогда, когда L = ⊤ и M = ⊤.

LaTeX

$$L.prod M = \\top \\iff L = \\top \\land M = \\top$$

Lean4

theorem pi_univ_eq_bot {L : ∀ i, Sublattice (π i)} {i : κ} (hL : L i = ⊥) : pi univ L = ⊥ :=
  pi_univ_eq_bot_iff.2 ⟨i, hL⟩

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

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

Разделы

Аффилиация

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