isGreatest_union_iff — Mathlib

English

IsGreatest(s ∪ t, a) holds iff either IsGreatest(s,a) and a ∈ upperBounds t, or a ∈ upperBounds s and IsGreatest t a.

Русский

IsGreatest( s ∪ t, a ) верно тогда и только тогда, когда IsGreatest(s,a) и a ∈ upperBounds(t), или a ∈ upperBounds(s) и IsGreatest(t,a).

LaTeX

$$$IsGreatest(s \\cup t, a) \\leftrightarrow (IsGreatest(s,a) \\land a \\in upperBounds(t)) \\lor (a \\in upperBounds(s) \\land IsGreatest(t,a))$$$

Lean4

theorem isGreatest_union_iff :
    IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a :=
  @isLeast_union_iff αᵒᵈ _ a s t

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