mk_inf_mk — Mathlib

English

The infimum (meet) of two opens corresponds to the intersection of their carriers with the open-ness preserved: ⟨U,V⟩ ⊓ ⟨W, h_W⟩ = ⟨U ∩ W, IsOpen.inter h_U h_W⟩.

Русский

Схождение двух открытых множеств соответствует пересечению их карриеров, сохраняющее открытость.

LaTeX

$$$\langle U, h_U \rangle \wedge \langle V, h_V \rangle = \langle U \cap V, \mathrm{IsOpen.inter} \, h_U \, h_V \rangle$$$

Lean4

@[simp]
theorem mk_inf_mk {U V : Set α} {hU : IsOpen U} {hV : IsOpen V} :
    (⟨U, hU⟩ ⊓ ⟨V, hV⟩ : Opens α) = ⟨U ⊓ V, IsOpen.inter hU hV⟩ :=
  rfl

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