disjoint_left — Mathlib

English

Disjoint s t is equivalent to ∀ a ∈ s, a ∉ t.

Русский

Непересечение множеств эквивалентно ∀ a ∈ s, a ∉ t.

LaTeX

$$$ \\operatorname{Disjoint}(s,t) \\Leftrightarrow \\forall a\\,(a \\in s \\rightarrow a \\notin t) $$$

Lean4

theorem disjoint_left : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t :=
  ⟨fun h a hs ht =>
    notMem_empty a <| singleton_subset_iff.mp (h (singleton_subset_iff.mpr hs) (singleton_subset_iff.mpr ht)),
    fun h _ hs ht _ ha => (h (hs ha) (ht ha)).elim⟩

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