pairwise_bot_iff — Mathlib

English

A set is pairwise with the bottom relation ⊥ iff it is subsingleton.

Русский

Множество попарно по отношению ⊥ тогда, когда оно subsingleton.

LaTeX

$$$\forall {s : Set \alpha}, s.Pairwise (\bot : \alpha \to \alpha \to \mathrm{Prop}) \iff s.Subsingleton$$$

Lean4

@[simp]
theorem pairwise_bot_iff : s.Pairwise (⊥ : α → α → Prop) ↔ (s : Set α).Subsingleton :=
  ⟨fun h _a ha _b hb => h.eq ha hb id, fun h => h.pairwise _⟩

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