disjoint_left — Mathlib

English

Disjoint s t iff for all a, a ∈ s implies a ∉ t.

Русский

Disjoint s t эквивалентно тому, что для всякого a, если a ∈ s, то a ∉ t.

LaTeX

$$$ \\mathrm{Disjoint}(s, t) \\iff \\forall a, a \\in s \\rightarrow a \\notin t $$$

Lean4

theorem disjoint_left {s t : Multiset α} : Disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
  by
  refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩
  · simpa using h (singleton_le.mpr hs) (singleton_le.mpr ht)
  · rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_notMem]
    exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

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