prod_eq_bot

Mathlib.Order.Sublattice

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

English

For Sublattices L ⊆ α and M ⊆ β, L.prod M = ⊥ iff L = ⊥ or M = ⊥.

Русский

Для подпределов L и M верно: L.prod M = ⊥ тогда и только тогда, когда L = ⊥ или M = ⊥.

LaTeX

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

Lean4

@[simp]
theorem prod_eq_bot {M : Sublattice β} : L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥ := by
  simpa only [← coe_inj] using Set.prod_eq_empty_iff

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

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

Разделы

Аффилиация

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