subgroup_strictAntiOn — Mathlib

English

The map s ↦ subgroup s is strictly Antitone on the interval Iio top, i.e. smaller upper sets give larger subgroups in a strict sense.

Русский

Отображение, сопоставляющее s подгруппу, является строго антиобратным на интервале Iio сверху.

LaTeX

$$StrictAntiOn (subgroup) (Set.Iio ⊤)$$

Lean4

@[to_additive]
theorem subgroup_strictAntiOn : StrictAntiOn (subgroup (M := M)) (Set.Iio ⊤) :=
  by
  intro s hs t ht hst
  rw [← SetLike.coe_ssubset_coe]
  rw [← subsemigroup_eq_subgroup_of_ne_top (Set.mem_Iio.mp hs).ne_top]
  rw [← subsemigroup_eq_subgroup_of_ne_top (Set.mem_Iio.mp ht).ne_top]
  refine Set.ssubset_iff_subset_ne.mpr ⟨by simpa [subsemigroup] using hst.le, ?_⟩
  contrapose! hst with heq
  apply le_of_eq
  simpa [mk_surjective, subsemigroup] using heq

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