infLELeft_apply — Mathlib

English

The left infimum embedding applied to U and V and an element x yields the corresponding left infimum element of U and V at x.

Русский

Применение левого вложения на U и V к элементу x даёт соответствующий элемент на x левого пересечения.

LaTeX

$$$(infLELeft U V) x = ⟨x, inf\_le\_left\; (U,V) x.2\rangle$$$

Lean4

theorem infLELeft_apply (U V : Opens X) (x) : (infLELeft U V) x = ⟨x.1, (@inf_le_left _ _ U V : _ ≤ _) x.2⟩ :=
  rfl

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