lowerPolar_union — Mathlib

English

Lower polar distributes over union: lowerPolar r (t1 ∪ t2) = lowerPolar r t1 ∩ lowerPolar r t2.

Русский

Lower polar распределяется по объединению: lowerPolar r (t1 ∪ t2) = lowerPolar r t1 ∩ lowerPolar r t2.

LaTeX

$$$\lowerPolar r (t_1 \cup t_2) = \lowerPolar r t_1 \cap \lowerPolar r t_2$$$

Lean4

@[simp]
theorem lowerPolar_union (t₁ t₂ : Set β) : lowerPolar r (t₁ ∪ t₂) = lowerPolar r t₁ ∩ lowerPolar r t₂ :=
  upperPolar_union ..

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