one_le_div_iff — Mathlib

English

If α is a Group, then 1 ≤ f / g is equivalent to ¬Disjoint f g.

Русский

Если α - группа, то 1 ≤ f / g эквивалентно ¬Disjoint f g.

LaTeX

$$1 ≤ f / g ↔ ¬Disjoint(f, g)$$

Lean4

@[to_additive (attr := simp high)] -- Ensure this fires before `le_div_iff`.

protected theorem one_le_div_iff : 1 ≤ f / g ↔ ¬Disjoint f g :=
  by
  refine ⟨fun h hfg => ?_, ?_⟩
  · obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)
    exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)
  · rintro h s ⟨t₁, h₁, t₂, h₂, hs⟩
    exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)

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