set_range_inclusion' — Mathlib

English

The range of the inclusion map on opens equals the underlying open set.

Русский

Область определения включения на открытых множествах равна исходному открытому множеству.

LaTeX

$$$\mathrm{Set.range}(\mathrm{inclusion'} U)=(U:\mathrm{Set}X).$$$

Lean4

theorem set_range_inclusion' {X : TopCat} (U : Opens X) : Set.range (inclusion' U) = (U : Set X) :=
  by
  ext x
  constructor
  · rintro ⟨x, rfl⟩
    exact x.2
  · intro h
    exact ⟨⟨x, h⟩, rfl⟩

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