intersecting_insert — Mathlib

English

Protected version of insert preserves the intersecting property under the same hypotheses as the unprotected version.

Русский

Защищённая версия вставки сохраняет свойство пересечения при тех же предположениях, что и несущая версия.

LaTeX

$$$$\\text{protected insert }(hs,a, h) : (insert a s).Intersecting.$$$$

Lean4

theorem intersecting_insert : (insert a s).Intersecting ↔ s.Intersecting ∧ a ≠ ⊥ ∧ ∀ b ∈ s, ¬Disjoint a b :=
  ⟨fun h =>
    ⟨h.mono <| subset_insert _ _, h.ne_bot <| mem_insert _ _, fun _b hb =>
      h (mem_insert _ _) <| mem_insert_of_mem _ hb⟩,
    fun h => h.1.insert h.2.1 h.2.2⟩

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