min'_union — Mathlib

English

For nonempty finite subsets S1 and S2, the minimum of their union equals the minimum of their minima, i.e. min(S1 ∪ S2) = min(min S1, min S2).

Русский

Для непустых конечных подмножеств S1 и S2 минимум их объединения равен минимуму минимумов: min(S1 ∪ S2) = min(min S1, min S2).

LaTeX

$$$\\min(S_1 \\cup S_2) = \\min\\big(\\min S_1, \\min S_2\\big).$$$

Lean4

theorem min'_union {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) :
    (s₁ ∪ s₂).min' (h₁.mono subset_union_left) = s₁.min' h₁ ⊓ s₂.min' h₂ :=
  inf'_union h₁ h₂ id

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