subgroup_antitone — Mathlib

English

The map s ↦ subgroup s is Antitone with respect to the order on UpperSet, i.e. larger upper sets give smaller subgroups.

Русский

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

LaTeX

$$Antitone (subgroup) (UpperSet.instTop.top)$$

Lean4

@[to_additive]
theorem subgroup_antitone : Antitone (subgroup (M := M)) :=
  by
  intro s t hst
  obtain rfl | hs := eq_or_ne s ⊤
  · rw [eq_top_iff.mpr hst]
  obtain rfl | ht := eq_or_ne t ⊤
  · simp
  rwa [subgroup_strictAntiOn.le_iff_ge ht.lt_top hs.lt_top]

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