leSupr_apply_mk — Mathlib

English

For a family U:ι → Opens X and i:ι, the inclusion from U_i to iSup U equals the iSup lifting at m.

Русский

Для семейства U_i и индекса i включение из U_i в iSup U равно тождественному отображению в iSup.

LaTeX

$$leSupr_apply_mk {ι} (U) (i) (x) (m) : (leSupr U i) ⟨x,m⟩ = ⟨x,(le_iSup U i) m⟩$$

Lean4

@[simp]
theorem leSupr_apply_mk {ι : Type*} (U : ι → Opens X) (i : ι) (x) (m) : (leSupr U i) ⟨x, m⟩ = ⟨x, (le_iSup U i :) m⟩ :=
  rfl

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