instInf — Mathlib

English

The meet (inf) of two definable sets corresponds to the intersection of their underlying sets.

Русский

Пересечение двух определяемых множеств соответствует пересечению их подмножеств функций.

LaTeX

$$$$ ((s \\cap t : L.DefinableSet A α) : Set(α \\to M)) = (s : Set(α \\to M)) \\cap (t : Set(α \\to M)). $$$$

Lean4

instance instInf : Min (L.DefinableSet A α) :=
  ⟨fun s t => ⟨s ∩ t, s.2.inter t.2⟩⟩

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