max'_union — Mathlib

English

For nonempty finite subsets S1 and S2, the maximum of their union equals the join of their maxima, i.e. max(S1 ∪ S2) = max(S1) ⊔ max(S2).

Русский

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

LaTeX

$$$\\max(S_1 \\cup S_2) = \\max\\left(\\max S_1, \\max S_2\\right).$$$

Lean4

theorem max'_union {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) :
    (s₁ ∪ s₂).max' (h₁.mono subset_union_left) = s₁.max' h₁ ⊔ s₂.max' h₂ :=
  sup'_union h₁ h₂ id

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