forall_ne_finset — Mathlib

English

The same as above, stated in the typical Finset notation: if h holds, then for any a in s and b in t, a ≠ b.

Русский

То же самое, но в стандартной нотации Finset: если выполнено h, то для любых a ∈ s и b ∈ t выполняется a ≠ b.

LaTeX

$$$ \\forall h:\\operatorname{Disjoint}(s,t), \\forall a\\in s, \\forall b\\in t, a \\neq b $$$

Lean4

theorem _root_.Disjoint.forall_ne_finset (h : Disjoint s t) (ha : a ∈ s) (hb : b ∈ t) : a ≠ b :=
  disjoint_iff_ne.1 h _ ha _ hb

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