English
The map t ↦ (t ∩ s, image under QuotientGroup.mk) is strictly monotone with respect to inclusion.
Русский
Отображение t ↦ (t ∩ s, образ через QuotientGroup.mk) строго монотонно по включению.
LaTeX
$$$\text{StrictMono}\; (t \mapsto (t \cap s, mk\,(s := s) '' t))$$$
Lean4
/-- Given a subgroup `s`, the function that sends a subgroup `t` to the pair consisting of
its intersection with `s` and its image in the quotient `α ⧸ s` is strictly monotone, even though
it is not injective in general. -/
@[to_additive QuotientAddGroup.strictMono_comap_prod_image /-- Given an additive subgroup `s`,
the function that sends an additive subgroup `t` to the pair consisting of
its intersection with `s` and its image in the quotient `α ⧸ s`
is strictly monotone, even though it is not injective in general. -/
]
theorem strictMono_comap_prod_image : StrictMono fun t : Subgroup α ↦ (t.comap s.subtype, mk (s := s) '' t) :=
by
refine fun t₁ t₂ h ↦ ⟨⟨Subgroup.comap_mono h.1, Set.image_mono h.1⟩, mt (fun ⟨le1, le2⟩ a ha ↦ ?_) h.2⟩
obtain ⟨a', h', eq⟩ := le2 ⟨_, ha, rfl⟩
convert ← t₁.mul_mem h' (@le1 ⟨_, QuotientGroup.eq.1 eq⟩ <| t₂.mul_mem (t₂.inv_mem <| h.1 h') ha)
apply mul_inv_cancel_left
