pi_univ_eq_bot_iff

Mathlib.Order.Sublattice

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

English

Equality characterization: L.prod M is bottom exactly when L or M is bottom.

Русский

Символическое равенство: L.prod M = ⊥, если и только если L = ⊥ или M = ⊥.

LaTeX

$$L.prod M = ⊥ \\iff L = ⊥ \\lor M = ⊥$$

Lean4

@[simp]
theorem pi_univ_eq_bot_iff {L : ∀ i, Sublattice (π i)} : pi univ L = ⊥ ↔ ∃ i, L i = ⊥ := by simp_rw [← coe_inj]; simp

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

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

Разделы

Аффилиация

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