coe_inf — Mathlib

English

The infimum of two congruences equals the infimum of their underlying binary relations: ↑(c ⊓ d) = ↑c ⊓ ↑d.

Русский

Предел двух конгруэнций равен пределу их бинарных отношений: ↑(c ⊓ d) = ↑c ⊓ ↑d.

LaTeX

$$$\\uparrow (c \\sqcap d) = \\uparrow c \\sqcap \\uparrow d$$$

Lean4

/-- The infimum of two congruence relations equals the infimum of the underlying binary
operations. -/
@[to_additive (attr := simp, norm_cast) /--
    The infimum of two additive congruence relations equals the infimum of the underlying binary
      operations. -/
    ]
theorem coe_inf {c d : Con M} : ⇑(c ⊓ d) = ⇑c ⊓ ⇑d :=
  rfl

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