infLELeft_apply_mk — Mathlib

English

For any U,V and x with a membership m in U ∩ V, the component of infLELeft at ⟨x,m⟩ is ⟨x, inf_left m⟩.

Русский

Для любого U,V и x с членством m в U ∩ V компонент инф_LEFT на ⟨x,m⟩ равен ⟨x, inf_left m⟩.

LaTeX

$$$ (infLELeft U V) ⟨x,m⟩ = ⟨x, (inf\_le\_left U V) m⟩ $$$

Lean4

@[simp]
theorem infLELeft_apply_mk (U V : Opens X) (x) (m) : (infLELeft U V) ⟨x, m⟩ = ⟨x, (@inf_le_left _ _ U V : _ ≤ _) m⟩ :=
  rfl

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