mem_sups — Mathlib

English

A general membership criterion: c ∈ s ⊻ t iff there exist a ∈ s, b ∈ t with a ⊔ b = c.

Русский

Обобщённое условие принадлежности: c ∈ s ⊻ t тогда и только тогда, когда существуют a ∈ s и b ∈ t такие, что a ⊔ b = c.

LaTeX

$$$ c \\in s \\oplus t \\iff \\exists a \\in s, \\exists b \\in t, a \\lor b = c $$$

Lean4

@[simp]
theorem mem_sups : c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c := by simp [(· ⊻ ·)]

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