mk_le_mk — Mathlib

English

For L,M Sublattice α with appropriate h-complements and bottoms, the relation mk L ... ≤ mk M ... holds if and only if L ≤ M.

Русский

Для подполуб (подалгебр) L и M из α с соответствующими доп. условиями верно: mk L ... ≤ mk M ... тогда и только тогда L ≤ M.

LaTeX

$$$mk\ L\ hL_{compl}\ hL_{bot} \le mk\ M\ hM_{compl}\ hM_{bot} \iff L \le M$$$

Lean4

@[simp]
theorem mk_le_mk {L M : Sublattice α} (hL_compl hL_bot hM_compl hM_bot) :
    mk L hL_compl hL_bot ≤ mk M hM_compl hM_bot ↔ L ≤ M :=
  .rfl

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