min_union — Mathlib

English

For finite subsets S and T of a linearly ordered set, the minimum of their union equals the minimum of the pair of minima: min(S ∪ T) = min(S) ⊓ min(T).

Русский

Для конечных подмножеств S и T линейно упорядоченного множества минимум их объединения равен минимуму двух минимумов: min(S ∪ T) = min(S) ⊓ min(T).

LaTeX

$$$$\min(S \cup T) = \min(S) \wedge \min(T).$$$$

Lean4

theorem min_union {s t : Finset α} : (s ∪ t).min = s.min ⊓ t.min :=
  inf_union

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