coe_inf — Mathlib

English

The coercion map preserves inf: the underlying element of the meet equals the meet of the underlying elements.

Русский

Включение сохраняет операцию meet: основанные элементы совпадают с их пересечением.

LaTeX

$$$\forall a,b\in \mathrm{Complementeds}(\alpha),\ \uparrow(a \land b) = (a : \alpha) \land (b : \alpha).$$$

Lean4

@[simp, norm_cast]
theorem coe_inf (a b : Complementeds α) : ↑(a ⊓ b) = (a : α) ⊓ b :=
  rfl

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