radical_sup — Mathlib

English

The radical distributes over addition: radical(I ⊔ J) = radical(radical(I) ⊔ radical(J)).

Русский

Радикал распространяется на сумму: √(I + J) = √(√I + √J).

LaTeX

$$$\\operatorname{radical}(I \\lor J) = \\operatorname{radical}(\\operatorname{radical}(I) \\lor \\operatorname{radical}(J))$$$

Lean4

theorem radical_sup : radical (I ⊔ J) = radical (radical I ⊔ radical J) :=
  le_antisymm (radical_mono <| sup_le_sup le_radical le_radical) <|
    radical_le_radical_iff.2 <| sup_le (radical_mono le_sup_left) (radical_mono le_sup_right)

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