ofList_append — Mathlib

English

The ideal generated by concatenation equals the sum of ideals generated by each part.

Русский

Идеал, порожденный rs1 ++ rs2, равен объединению порожденных rs1 и rs2.

LaTeX

$$$\\text{Ideal.ofList}(rs_1 \\;\\text{++}\\; rs_2) = \\text{Ideal.ofList}(rs_1) \\;\\sqcup\\; \\text{Ideal.ofList}(rs_2)$$$

Lean4

@[simp]
theorem ofList_append (rs₁ rs₂ : List R) : ofList (rs₁ ++ rs₂) = ofList rs₁ ⊔ ofList rs₂ :=
  have : {r | r ∈ rs₁ ++ rs₂} = _ := Set.ext (fun _ => List.mem_append)
  Eq.trans (congrArg span this) (span_union _ _)

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