Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov
! This file was ported from Lean 3 source module algebra.bounds
! leanprover-community/mathlib commit dd71334db81d0bd444af1ee339a29298bef40734
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.Group.OrderIso
import Mathlib.Algebra.Order.Monoid.OrderDual
import Mathlib.Data.Set.Pointwise.Basic
import Mathlib.Order.Bounds.OrderIso
import Mathlib.Order.ConditionallyCompleteLattice.Basic
/-!
# Upper/lower bounds in ordered monoids and groups
In this file we prove a few facts like “`-s` is bounded above iff `s` is bounded below”
(`bddAbove_neg`).
-/
open Function Set
open Pointwise
section InvNeg
variable { G : Type _ } [ Group G ] [ Preorder G ] [ CovariantClass : (M : Type ?u.12) → (N : Type ?u.11) → (M → N → N (N → N → Prop Prop G G (· * ·) (· ≤ ·) ]
[ CovariantClass : (M : Type ?u.6658) → (N : Type ?u.6657) → (M → N → N (N → N → Prop Prop G G ( swap : {α : Sort ?u.659} →
{β : Sort ?u.658} → {φ : α → β → Sort ?u.657((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· * ·) ) (· ≤ ·) ] { s : Set G } { a : G }
@[ to_additive ( attr := simp )]
theorem bddAbove_inv : BddAbove s ⁻¹ ↔ BddBelow s :=
( OrderIso.inv G ). bddAbove_preimage
#align bdd_above_inv bddAbove_inv
#align bdd_above_neg bddAbove_neg
@[ to_additive ( attr := simp )]
theorem bddBelow_inv : BddBelow s ⁻¹ ↔ BddAbove s :=
( OrderIso.inv G ). bddBelow_preimage
#align bdd_below_inv bddBelow_inv
#align bdd_below_neg bddBelow_neg
@[ to_additive ]
theorem BddAbove.inv ( h : BddAbove s ) : BddBelow s ⁻¹ :=
bddBelow_inv . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
#align bdd_above.inv BddAbove.inv
#align bdd_above.neg BddAbove.neg
@[ to_additive ]
theorem BddBelow.inv ( h : BddBelow s ) : BddAbove s ⁻¹ :=
bddAbove_inv . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
#align bdd_below.inv BddBelow.inv
#align bdd_below.neg BddBelow.neg
@[ to_additive ( attr := simp )]
theorem isLUB_inv : IsLUB s ⁻¹ a ↔ IsGLB s a ⁻¹ :=
( OrderIso.inv G ). isLUB_preimage
#align is_lub_inv isLUB_inv
#align is_lub_neg isLUB_neg
@[ to_additive ]
theorem isLUB_inv' : IsLUB s ⁻¹ a ⁻¹ ↔ IsGLB s a :=
( OrderIso.inv G ). isLUB_preimage'
#align is_lub_inv' isLUB_inv'
#align is_lub_neg' isLUB_neg'
@[ to_additive ]
theorem IsGLB.inv ( h : IsGLB s a ) : IsLUB s ⁻¹ a ⁻¹ :=
isLUB_inv' . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
#align is_glb.inv IsGLB.inv
#align is_glb.neg IsGLB.neg
@[ to_additive ( attr := simp )]
theorem isGLB_inv : IsGLB s ⁻¹ a ↔ IsLUB s a ⁻¹ :=
( OrderIso.inv G ). isGLB_preimage
#align is_glb_inv isGLB_inv
#align is_glb_neg isGLB_neg
@[ to_additive ]
theorem isGLB_inv' : IsGLB s ⁻¹ a ⁻¹ ↔ IsLUB s a :=
( OrderIso.inv G ). isGLB_preimage'
#align is_glb_inv' isGLB_inv'
#align is_glb_neg' isGLB_neg'
@[ to_additive ]
theorem IsLUB.inv ( h : IsLUB s a ) : IsGLB s ⁻¹ a ⁻¹ :=
isGLB_inv' . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
#align is_lub.inv IsLUB.inv
#align is_lub.neg IsLUB.neg
end InvNeg
section mul_add
variable { M : Type _ : Type (?u.18454+1)} [ Mul M ] [ Preorder M ] [ CovariantClass : (M : Type ?u.19895) → (N : Type ?u.19894) → (M → N → N (N → N → Prop Prop M M (· * ·) (· ≤ ·) ]
[ CovariantClass : (M : Type ?u.18546) → (N : Type ?u.18545) → (M → N → N (N → N → Prop Prop M M ( swap : {α : Sort ?u.19206} →
{β : Sort ?u.19205} → {φ : α → β → Sort ?u.19204((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· * ·) ) (· ≤ ·) ]
@[ to_additive ]
theorem mul_mem_upperBounds_mul { s t : Set M } { a b : M } ( ha : a ∈ upperBounds s )
( hb : b ∈ upperBounds t ) : a * b ∈ upperBounds ( s * t ) :=
forall_image2_iff : ∀ {α : Type ?u.18113} {β : Type ?u.18114} {γ : Type ?u.18112} {f : α → β → γ s : Set α t : Set β p : γ → Prop (∀ (z : γ ), z ∈ image2 f s t p z ) ↔ ∀ (x : α ), x ∈ s ∀ (y : β ), y ∈ t p (f x y . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _ hx _ hy => mul_le_mul' ( ha hx ) ( hb hy )
#align mul_mem_upper_bounds_mul mul_mem_upperBounds_mul
#align add_mem_upper_bounds_add add_mem_upperBounds_add
@[ to_additive ]
theorem subset_upperBounds_mul ( s t : Set M ) :
upperBounds s * upperBounds t ⊆ upperBounds ( s * t ) :=
image2_subset_iff : ∀ {α : Type ?u.18806} {β : Type ?u.18807} {γ : Type ?u.18805} {f : α → β → γ s : Set α t : Set β u : Set γ image2 f s t ⊆ u ↔ ∀ (x : α ), x ∈ s ∀ (y : β ), y ∈ t f x y ∈ u . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun _ hx _ hy => mul_mem_upperBounds_mul hx hy
#align subset_upper_bounds_mul subset_upperBounds_mul
#align subset_upper_bounds_add subset_upperBounds_add
@[ to_additive ]
theorem mul_mem_lowerBounds_mul { s t : Set M } { a b : M } ( ha : a ∈ lowerBounds s )
( hb : b ∈ lowerBounds t ) : a * b ∈ lowerBounds ( s * t ) :=
@ mul_mem_upperBounds_mul M ᵒᵈ _ _ _ _ _ _ _ _ ha hb
#align mul_mem_lower_bounds_mul mul_mem_lowerBounds_mul
#align add_mem_lower_bounds_add add_mem_lowerBounds_add
@[ to_additive ]
theorem subset_lowerBounds_mul ( s t : Set M ) :
lowerBounds s * lowerBounds t ⊆ lowerBounds ( s * t ) :=
@ subset_upperBounds_mul M ᵒᵈ _ _ _ _ _ _
#align subset_lower_bounds_mul subset_lowerBounds_mul
#align subset_lower_bounds_add subset_lowerBounds_add
@[ to_additive ]
theorem BddAbove.mul { s t : Set M } ( hs : BddAbove s ) ( ht : BddAbove t ) : BddAbove ( s * t ) :=
( Nonempty.mul hs ht ). mono ( subset_upperBounds_mul s t )
#align bdd_above.mul BddAbove.mul
#align bdd_above.add BddAbove.add
@[ to_additive ]
theorem BddBelow.mul { s t : Set M } ( hs : BddBelow s ) ( ht : BddBelow t ) : BddBelow ( s * t ) :=
( Nonempty.mul hs ht ). mono ( subset_lowerBounds_mul s t )
#align bdd_below.mul BddBelow.mul
#align bdd_below.add BddBelow.add
end mul_add
section ConditionallyCompleteLattice
section Right
variable { ι G : Type _ : Type (?u.22515+1)} [ Group G ] [ ConditionallyCompleteLattice : Type ?u.21555 → Type ?u.21555 G ]
[ CovariantClass : (M : Type ?u.21559) → (N : Type ?u.21558) → (M → N → N (N → N → Prop Prop G G ( Function.swap : {α : Sort ?u.21562} →
{β : Sort ?u.21561} → {φ : α → β → Sort ?u.21560((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· * ·) ) (· ≤ ·) ] [ Nonempty ι ] { f : ι → G }
@[ to_additive ]
theorem ciSup_mul ( hf : BddAbove ( Set.range : {α : Type ?u.23498} → {ι : Sort ?u.23497} → (ι → α Set α f )) ( a : G ) : (⨆ i , f i ) * a = ⨆ i , f i * a :=
( OrderIso.mulRight : {α : Type ?u.24719} →
[inst : Group α [inst_1 : LE α [inst : CovariantClass α α (swap fun x x_1 => x * x_1 fun x x_1 => x ≤ x_1 α → α ≃o α a ). map_ciSup hf
#align csupr_mul ciSup_mul
#align csupr_add ciSup_add
@[ to_additive ]
theorem ciSup_div ( hf : BddAbove ( Set.range : {α : Type ?u.26246} → {ι : Sort ?u.26245} → (ι → α Set α f )) ( a : G ) : (⨆ i , f i ) / a = ⨆ i , f i / a := by
(⨆ i , f i ) / a = ⨆ i , f i / a simp only [ div_eq_mul_inv , ciSup_mul hf ]
#align csupr_div ciSup_div
#align csupr_sub ciSup_sub
end Right
section Left
variable { ι G : Type _ : Type (?u.27173+1)} [ Group G ] [ ConditionallyCompleteLattice : Type ?u.27179 → Type ?u.27179 G ]
[ CovariantClass : (M : Type ?u.28127) → (N : Type ?u.28126) → (M → N → N (N → N → Prop Prop G G (· * ·) (· ≤ ·) ] [ Nonempty ι ] { f : ι → G }
@[ to_additive ]
theorem mul_ciSup ( hf : BddAbove ( Set.range : {α : Type ?u.29078} → {ι : Sort ?u.29077} → (ι → α Set α f )) ( a : G ) : ( a * ⨆ i , f i ) = ⨆ i , a * f i :=
( OrderIso.mulLeft : {α : Type ?u.30299} →
[inst : Group α [inst_1 : LE α [inst : CovariantClass α α (fun x x_1 => x * x_1 ) fun x x_1 => x ≤ x_1 α → α ≃o α a ). map_ciSup hf
#align mul_csupr mul_ciSup
#align add_csupr add_ciSup
end Left
end ConditionallyCompleteLattice