prod_eq_top — Mathlib

English

If L and M are Sublattices of α and β, then L.prod M = ⊤ iff L = ⊤ and M = ⊤ (assuming nonempty types).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem prod_eq_top [Nonempty α] [Nonempty β] {M : Sublattice β} : L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤ := by
  simpa only [← coe_inj] using Set.prod_eq_univ

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