add_eq_union_left_of_le — Mathlib

English

If t ≤ s, then u + s = u ∪ t iff Disjoint u s ∧ s = t.

Русский

Пусть t ≤ s. Тогда u + s = u ∪ t эквивалентно Disjoint u s ∧ s = t.

LaTeX

$$$t \\le s \\Rightarrow (u + s) = (u \\cup t) \\iff (Disjoint u s) \\land s = t$$$

Lean4

theorem add_eq_union_left_of_le [DecidableEq α] {s t u : Multiset α} (h : t ≤ s) :
    u + s = u ∪ t ↔ Disjoint u s ∧ s = t :=
  by
  rw [← add_eq_union_iff_disjoint]
  refine ⟨fun h0 ↦ ?_, ?_⟩
  · rw [and_iff_right_of_imp]
    · exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h
    · rintro rfl
      exact h0
  · rintro ⟨h0, rfl⟩
    exact h0

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