upperPolar_union — Mathlib

English

Upper polar distributes over union: upperPolar r (s1 ∪ s2) = upperPolar r s1 ∩ upperPolar r s2.

Русский

Upper polar распределяется по объединению: upperPolar r (s1 ∪ s2) = upperPolar r s1 ∩ upperPolar r s2.

LaTeX

$$$\upperPolar r (s_1 \cup s_2) = \upperPolar r s_1 \cap \upperPolar r s_2$$$

Lean4

@[simp]
theorem upperPolar_union (s₁ s₂ : Set α) : upperPolar r (s₁ ∪ s₂) = upperPolar r s₁ ∩ upperPolar r s₂ :=
  ext fun _ => forall₂_or_left

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