le_prod_iff

Mathlib.Order.Sublattice

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

← MathLib Explorer

English

For N ≤ L.prod M, this is equivalent to N ≤ comap fst L and N ≤ comap snd M.

Русский

Для N ≤ L.prod M равносильно N ≤ comap fst L и N ≤ comap snd M.

LaTeX

$$N \\le L.prod M \\iff N \\le comap( fst ) L \\wedge N \\le comap( snd ) M$$

Lean4

theorem le_prod_iff {M : Sublattice β} {N : Sublattice (α × β)} :
    N ≤ L.prod M ↔ N ≤ comap LatticeHom.fst L ∧ N ≤ comap LatticeHom.snd M := by simp [SetLike.le_def, forall_and]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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