isLeast_union_iff — Mathlib

English

IsLeast(s ∪ t, a) holds iff either a is least in s and a ∈ lowerBounds t, or a ∈ lowerBounds s and a is least in t.

Русский

IsLeast( s ∪ t, a ) эквивалентно либо IsLeast(s,a) и a ∈ lowerBounds(t), либо a ∈ lowerBounds(s) и IsLeast(t,a).

LaTeX

$$$IsLeast(s \\cup t, a) \\leftrightarrow (IsLeast(s,a) \\land a \\in \\mathrm{lowerBounds}(t)) \\lor (a \\in \\mathrm{lowerBounds}(s) \\land IsLeast(t,a))$$$

Lean4

theorem isLeast_union_iff {a : α} {s t : Set α} :
    IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a := by
  simp [IsLeast, lowerBounds_union, or_and_right, and_comm (a := a ∈ t), and_assoc]

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