pairwise_insert_of_symmetric_of_notMem

English

If r is symmetric and a ∉ s, then (insert a s) is pairwise w.r.t r iff s is pairwise w.r.t r and ∀ b ∈ s, r a b.

Русский

Если r симметрично и a не в s, то (insert a s) попарно по r тогда и только тогда, когда s попарно по r и ∀ b ∈ s, r a b.

LaTeX

$$$(\text{hr}) \Rightarrow ((insert a s).Pairwise r) \leftrightarrow (s.Pairwise r \land \forall b \in s, r a b)$$$

Lean4

theorem pairwise_insert_of_symmetric_of_notMem (hr : Symmetric r) (ha : a ∉ s) :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b := by
  simp only [pairwise_insert_of_notMem ha, hr.iff a, and_self_iff]

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