mem_disjSups — Mathlib

English

Characterization of membership in disjSups: c ∈ s ○ t iff there exist a ∈ s and b ∈ t with Disjoint(a,b) and a ⊔ b = c.

Русский

Характеризация члена множества s ○ t: c ∈ s ○ t тогда и только тогда, когда существует a ∈ s и b ∈ t такие, что Disjoint(a,b) и a ⊔ b = c.

LaTeX

$$$ c \in s \circ t \iff \exists a \in s, \exists b \in t, Disjoint(a,b) \land a \vee b = c $$$

Lean4

@[simp]
theorem mem_disjSups : c ∈ s ○ t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c := by simp [disjSups, and_assoc]

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