ι_preimage_self — Mathlib

English

Let U be an open subset of X with inclusion i: U → X. The pullback of U along this inclusion is the entire space U; i.e., the preimage of U under the inclusion equals the top element in the lattice of opens of U.

Русский

Пусть U — открытое подмножество X, и i: U → X — вложение. Тогда предобраз U по вложению равен всему U; т.е. i^{-1}(U) = ⊤ в Решении открытых подмножеств U.

LaTeX

$$$ U.\\iota^{-1}_{\\mathcal{U}} U = \\top $$$

Lean4

@[simp]
theorem ι_preimage_self : U.ι ⁻¹ᵁ U = ⊤ :=
  Opens.inclusion'_map_eq_top _

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