cofinite_inf_principal_diff — Mathlib

English

If t is finite, then cofinite ∧ principal(s \ t) = cofinite ∧ principal(s).

Русский

Если t конечна, то cofinite ∧ principal(s \\ t) = cofinite ∧ principal(s).

LaTeX

$$$\\operatorname{cofinite} \\wedge \\mathcal{P}(s \\setminus t) = \\operatorname{cofinite} \\wedge \\mathcal{P}(s)$$$

Lean4

theorem cofinite_inf_principal_diff {s t : Set α} (ht : t.Finite) : cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s := by
  rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]

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