sep_sups_le — Mathlib

English

Separating sa sets with a bound a: {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}.

Русский

Разделение по ограничению: {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}.

LaTeX

$$$ \\{b \\in s \\veebar t \\mid b \\le a\\} = \\{b \\in s \\mid b \\le a\\} \\veebar \\{b \\in t \\mid b \\le a\\} $$$

Lean4

theorem sep_sups_le (s t : Set α) (a : α) : {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a} := by ext; aesop

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