preimage_compl — Mathlib

English

If s is an antichain in α, then the preimage of s under the complement map is an antichain in α.

Русский

Если s является антицепочкой в α, то предобраз дополнения s по карте дополнения — антицепочочка.

LaTeX

$$$IsAntichain(\le)(\mathrm{compl}^{-1}(s))$$$

Lean4

theorem preimage_compl [BooleanAlgebra α] (hs : IsAntichain (· ≤ ·) s) : IsAntichain (· ≤ ·) (compl ⁻¹' s) :=
  fun _ ha _ ha' hne hle => hs ha' ha (fun h => hne (compl_inj_iff.mp h.symm)) (compl_le_compl hle)

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