instInf — Mathlib

English

The infimum of two compact-opens is given by their intersection of carriers.

Русский

Наименьшее совместное надмножество двух компактно-открытых дается пересечением их носителей.

LaTeX

$$$\uparrow (U \wedge V) = U \cap V$$$

Lean4

instance instInf : Min (CompactOpens α) where
  min U V := ⟨⟨U ∩ V, QuasiSeparatedSpace.inter_isCompact U.1.1 V.1.1 U.2 U.1.2 V.2 V.1.2⟩, U.2.inter V.2⟩

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