coe_inf — Mathlib

English

In the interval Icc(a,b) with a ≤ b, the coercion map from the interval to α preserves infima; namely, for x,y ∈ Icc(a,b), the image of their infimum equals the infimum of their images: ↑(x ⊓ y) = ↑x ⊓ ↑y.

Русский

Для любых x,y ∈ Icc(a,b) выполняется, что образ их пересечения через включение в α равен пересечению образов: ↑(x ⊓ y) = ↑x ⊓ ↑y.

LaTeX

$$$\uparrow(x \wedge y) = (\uparrow x) \wedge (\uparrow y).$$$

Lean4

@[simp, norm_cast]
protected theorem coe_inf [SemilatticeInf α] {x y : Icc a b} : ↑(x ⊓ y) = (↑x ⊓ ↑y : α) :=
  rfl

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