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 Cmdinstead 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 ?u.15836
G
:
Type _: Type (?u.7586+1)
Type _
} [
Group: Type ?u.5 → Type ?u.5
Group
G: Type ?u.2832
G
] [
Preorder: Type ?u.15842 → Type ?u.15842
Preorder
G: Type ?u.7586
G
] [
CovariantClass: (M : Type ?u.12) → (N : Type ?u.11) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
G: Type ?u.2
G
G: Type ?u.2
G
(· * ·): G → G → G
(· * ·)
(· ≤ ·): G → G → Prop
(· ≤ ·)
] [
CovariantClass: (M : Type ?u.6658) → (N : Type ?u.6657) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
G: Type ?u.2
G
G: Type ?u.2
G
(
swap: {α : Sort ?u.659} → {β : Sort ?u.658} → {φ : α → β → Sort ?u.657} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): G → G → G
(· * ·)
)
(· ≤ ·): G → G → Prop
(· ≤ ·)
] {
s: Set G
s
:
Set: Type ?u.1237 → Type ?u.1237
Set
G: Type ?u.2
G
} {
a: G
a
:
G: Type ?u.2
G
} @[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove (-s) ↔ BddBelow s
to_additive
(attr := simp)] theorem
bddAbove_inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove s⁻¹ ↔ BddBelow s
bddAbove_inv
:
BddAbove: {α : Type ?u.2482} → [inst : Preorder α] → Set α → Prop
BddAbove
s: Set G
s
⁻¹ ↔
BddBelow: {α : Type ?u.2586} → [inst : Preorder α] → Set α → Prop
BddBelow
s: Set G
s
:= (
OrderIso.inv: (α : Type ?u.2592) → [inst : Group α] → [inst_1 : LE α] → [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → [inst : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → α ≃o αᵒᵈ
OrderIso.inv
G: Type ?u.1242
G
).
bddAbove_preimage: ∀ {α : Type ?u.2652} {β : Type ?u.2651} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set β}, BddAbove (↑e ⁻¹' s) ↔ BddAbove s
bddAbove_preimage
#align bdd_above_inv
bddAbove_inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove s⁻¹ ↔ BddBelow s
bddAbove_inv
#align bdd_above_neg
bddAbove_neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove (-s) ↔ BddBelow s
bddAbove_neg
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow (-s) ↔ BddAbove s
to_additive
(attr := simp)] theorem
bddBelow_inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow s⁻¹ ↔ BddAbove s
bddBelow_inv
:
BddBelow: {α : Type ?u.4072} → [inst : Preorder α] → Set α → Prop
BddBelow
s: Set G
s
⁻¹ ↔
BddAbove: {α : Type ?u.4176} → [inst : Preorder α] → Set α → Prop
BddAbove
s: Set G
s
:= (
OrderIso.inv: (α : Type ?u.4182) → [inst : Group α] → [inst_1 : LE α] → [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → [inst : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → α ≃o αᵒᵈ
OrderIso.inv
G: Type ?u.2832
G
).
bddBelow_preimage: ∀ {α : Type ?u.4242} {β : Type ?u.4241} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set β}, BddBelow (↑e ⁻¹' s) ↔ BddBelow s
bddBelow_preimage
#align bdd_below_inv
bddBelow_inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow s⁻¹ ↔ BddAbove s
bddBelow_inv
#align bdd_below_neg
bddBelow_neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow (-s) ↔ BddAbove s
bddBelow_neg
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove s → BddBelow (-s)
to_additive
] theorem
BddAbove.inv: BddAbove s → BddBelow s⁻¹
BddAbove.inv
(h :
BddAbove: {α : Type ?u.5662} → [inst : Preorder α] → Set α → Prop
BddAbove
s: Set G
s
) :
BddBelow: {α : Type ?u.5688} → [inst : Preorder α] → Set α → Prop
BddBelow
s: Set G
s
⁻¹ :=
bddBelow_inv: ∀ {G : Type ?u.5804} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow s⁻¹ ↔ BddAbove s
bddBelow_inv
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
h #align bdd_above.inv
BddAbove.inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove s → BddBelow s⁻¹
BddAbove.inv
#align bdd_above.neg
BddAbove.neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove s → BddBelow (-s)
BddAbove.neg
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow s → BddAbove (-s)
to_additive
] theorem
BddBelow.inv: BddBelow s → BddAbove s⁻¹
BddBelow.inv
(h :
BddBelow: {α : Type ?u.7244} → [inst : Preorder α] → Set α → Prop
BddBelow
s: Set G
s
) :
BddAbove: {α : Type ?u.7270} → [inst : Preorder α] → Set α → Prop
BddAbove
s: Set G
s
⁻¹ :=
bddAbove_inv: ∀ {G : Type ?u.7386} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddAbove s⁻¹ ↔ BddBelow s
bddAbove_inv
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
h #align bdd_below.inv
BddBelow.inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow s → BddAbove s⁻¹
BddBelow.inv
#align bdd_below.neg
BddBelow.neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G}, BddBelow s → BddAbove (-s)
BddBelow.neg
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB (-s) a ↔ IsGLB s (-a)
to_additive
(attr := simp)] theorem isLUB_inv :
IsLUB: {α : Type ?u.8826} → [inst : Preorder α] → Set α → α → Prop
IsLUB
s: Set G
s
⁻¹
a: G
a
↔
IsGLB: {α : Type ?u.8930} → [inst : Preorder α] → Set α → α → Prop
IsGLB
s: Set G
s
a: G
a
⁻¹ := (
OrderIso.inv: (α : Type ?u.9001) → [inst : Group α] → [inst_1 : LE α] → [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → [inst : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → α ≃o αᵒᵈ
OrderIso.inv
G: Type ?u.7586
G
).
isLUB_preimage: ∀ {α : Type ?u.9061} {β : Type ?u.9060} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : α}, IsLUB (↑f ⁻¹' s) x ↔ IsLUB s (↑f x)
isLUB_preimage
#align is_lub_inv
isLUB_inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB s⁻¹ a ↔ IsGLB s a⁻¹
isLUB_inv
#align is_lub_neg
isLUB_neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB (-s) a ↔ IsGLB s (-a)
isLUB_neg
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB (-s) (-a) ↔ IsGLB s a
to_additive
] theorem isLUB_inv' :
IsLUB: {α : Type ?u.10509} → [inst : Preorder α] → Set α → α → Prop
IsLUB
s: Set G
s
⁻¹
a: G
a
⁻¹ ↔
IsGLB: {α : Type ?u.10678} → [inst : Preorder α] → Set α → α → Prop
IsGLB
s: Set G
s
a: G
a
:= (
OrderIso.inv: (α : Type ?u.10684) → [inst : Group α] → [inst_1 : LE α] → [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → [inst : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → α ≃o αᵒᵈ
OrderIso.inv
G: Type ?u.9269
G
).
isLUB_preimage': ∀ {α : Type ?u.10744} {β : Type ?u.10743} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : β}, IsLUB (↑f ⁻¹' s) (↑(OrderIso.symm f) x) ↔ IsLUB s x
isLUB_preimage'
#align is_lub_inv'
isLUB_inv': ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a
isLUB_inv'
#align is_lub_neg'
isLUB_neg': ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB (-s) (-a) ↔ IsGLB s a
isLUB_neg'
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB s a → IsLUB (-s) (-a)
to_additive
] theorem
IsGLB.inv: IsGLB s a → IsLUB s⁻¹ a⁻¹
IsGLB.inv
(
h: IsGLB s a
h
:
IsGLB: {α : Type ?u.12124} → [inst : Preorder α] → Set α → α → Prop
IsGLB
s: Set G
s
a: G
a
) :
IsLUB: {α : Type ?u.12150} → [inst : Preorder α] → Set α → α → Prop
IsLUB
s: Set G
s
⁻¹
a: G
a
⁻¹ :=
isLUB_inv': ∀ {G : Type ?u.12331} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a
isLUB_inv'
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
h: IsGLB s a
h
#align is_glb.inv
IsGLB.inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB s a → IsLUB s⁻¹ a⁻¹
IsGLB.inv
#align is_glb.neg
IsGLB.neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB s a → IsLUB (-s) (-a)
IsGLB.neg
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB (-s) a ↔ IsLUB s (-a)
to_additive
(attr := simp)] theorem isGLB_inv :
IsGLB: {α : Type ?u.13778} → [inst : Preorder α] → Set α → α → Prop
IsGLB
s: Set G
s
⁻¹
a: G
a
↔
IsLUB: {α : Type ?u.13882} → [inst : Preorder α] → Set α → α → Prop
IsLUB
s: Set G
s
a: G
a
⁻¹ := (
OrderIso.inv: (α : Type ?u.13953) → [inst : Group α] → [inst_1 : LE α] → [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → [inst : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → α ≃o αᵒᵈ
OrderIso.inv
G: Type ?u.12538
G
).
isGLB_preimage: ∀ {α : Type ?u.14013} {β : Type ?u.14012} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : α}, IsGLB (↑f ⁻¹' s) x ↔ IsGLB s (↑f x)
isGLB_preimage
#align is_glb_inv
isGLB_inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB s⁻¹ a ↔ IsLUB s a⁻¹
isGLB_inv
#align is_glb_neg
isGLB_neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB (-s) a ↔ IsLUB s (-a)
isGLB_neg
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB (-s) (-a) ↔ IsLUB s a
to_additive
] theorem
isGLB_inv': ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a
isGLB_inv'
:
IsGLB: {α : Type ?u.15461} → [inst : Preorder α] → Set α → α → Prop
IsGLB
s: Set G
s
⁻¹
a: G
a
⁻¹ ↔
IsLUB: {α : Type ?u.15630} → [inst : Preorder α] → Set α → α → Prop
IsLUB
s: Set G
s
a: G
a
:= (
OrderIso.inv: (α : Type ?u.15636) → [inst : Group α] → [inst_1 : LE α] → [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → [inst : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] → α ≃o αᵒᵈ
OrderIso.inv
G: Type ?u.14221
G
).
isGLB_preimage': ∀ {α : Type ?u.15696} {β : Type ?u.15695} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : β}, IsGLB (↑f ⁻¹' s) (↑(OrderIso.symm f) x) ↔ IsGLB s x
isGLB_preimage'
#align is_glb_inv'
isGLB_inv': ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a
isGLB_inv'
#align is_glb_neg'
isGLB_neg': ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB (-s) (-a) ↔ IsLUB s a
isGLB_neg'
@[
to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB s a → IsGLB (-s) (-a)
to_additive
] theorem
IsLUB.inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB s a → IsGLB s⁻¹ a⁻¹
IsLUB.inv
(
h: IsLUB s a
h
:
IsLUB: {α : Type ?u.17076} → [inst : Preorder α] → Set α → α → Prop
IsLUB
s: Set G
s
a: G
a
) :
IsGLB: {α : Type ?u.17102} → [inst : Preorder α] → Set α → α → Prop
IsGLB
s: Set G
s
⁻¹
a: G
a
⁻¹ :=
isGLB_inv': ∀ {G : Type ?u.17283} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a
isGLB_inv'
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
h: IsLUB s a
h
#align is_lub.inv
IsLUB.inv: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB s a → IsGLB s⁻¹ a⁻¹
IsLUB.inv
#align is_lub.neg
IsLUB.neg: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Preorder G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s : Set G} {a : G}, IsLUB s a → IsGLB (-s) (-a)
IsLUB.neg
end InvNeg section mul_add variable {
M: Type ?u.17671
M
:
Type _: Type (?u.18454+1)
Type _
} [
Mul: Type ?u.19114 → Type ?u.19114
Mul
M: Type ?u.17490
M
] [
Preorder: Type ?u.21055 → Type ?u.21055
Preorder
M: Type ?u.19111
M
] [
CovariantClass: (M : Type ?u.19895) → (N : Type ?u.19894) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
M: Type ?u.17490
M
M: Type ?u.17671
M
(· * ·): M → M → M
(· * ·)
(· ≤ ·): M → M → Prop
(· ≤ ·)
] [
CovariantClass: (M : Type ?u.18546) → (N : Type ?u.18545) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
M: Type ?u.19111
M
M: Type ?u.19111
M
(
swap: {α : Sort ?u.19206} → {β : Sort ?u.19205} → {φ : α → β → Sort ?u.19204} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): M → M → M
(· * ·)
)
(· ≤ ·): M → M → Prop
(· ≤ ·)
] @[
to_additive: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ upperBounds s → b ∈ upperBounds t → a + b ∈ upperBounds (s + t)
to_additive
] theorem
mul_mem_upperBounds_mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ upperBounds s → b ∈ upperBounds t → a * b ∈ upperBounds (s * t)
mul_mem_upperBounds_mul
{
s: Set M
s
t: Set M
t
:
Set: Type ?u.17855 → Type ?u.17855
Set
M: Type ?u.17671
M
} {
a: M
a
b: M
b
:
M: Type ?u.17671
M
} (ha :
a: M
a
∈
upperBounds: {α : Type ?u.17877} → [inst : Preorder α] → Set α → Set α
upperBounds
s: Set M
s
) (hb :
b: M
b
∈
upperBounds: {α : Type ?u.17929} → [inst : Preorder α] → Set α → Set α
upperBounds
t: Set M
t
) :
a: M
a
*
b: M
b
∈
upperBounds: {α : Type ?u.18016} → [inst : Preorder α] → Set α → Set α
upperBounds
(
s: Set M
s
*
t: Set M
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)
forall_image2_iff
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
fun
_: ?m.18162
_
hx: ?m.18165
hx
_: ?m.18168
_
hy: ?m.18171
hy
=>
mul_le_mul': ∀ {α : Type ?u.18173} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c d : α}, a ≤ b → c ≤ d → a * c ≤ b * d
mul_le_mul'
(ha
hx: ?m.18165
hx
) (hb
hy: ?m.18171
hy
) #align mul_mem_upper_bounds_mul
mul_mem_upperBounds_mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ upperBounds s → b ∈ upperBounds t → a * b ∈ upperBounds (s * t)
mul_mem_upperBounds_mul
#align add_mem_upper_bounds_add
add_mem_upperBounds_add: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ upperBounds s → b ∈ upperBounds t → a + b ∈ upperBounds (s + t)
add_mem_upperBounds_add
@[
to_additive: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (s t : Set M), upperBounds s + upperBounds t ⊆ upperBounds (s + t)
to_additive
] theorem
subset_upperBounds_mul: ∀ (s t : Set M), upperBounds s * upperBounds t ⊆ upperBounds (s * t)
subset_upperBounds_mul
(
s: Set M
s
t: Set M
t
:
Set: Type ?u.18635 → Type ?u.18635
Set
M: Type ?u.18454
M
) :
upperBounds: {α : Type ?u.18652} → [inst : Preorder α] → Set α → Set α
upperBounds
s: Set M
s
*
upperBounds: {α : Type ?u.18663} → [inst : Preorder α] → Set α → Set α
upperBounds
t: Set M
t
⊆
upperBounds: {α : Type ?u.18736} → [inst : Preorder α] → Set α → Set α
upperBounds
(
s: Set M
s
*
t: Set M
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
image2_subset_iff
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
fun
_: ?m.18846
_
hx: ?m.18849
hx
_: ?m.18852
_
hy: ?m.18855
hy
=>
mul_mem_upperBounds_mul: ∀ {M : Type ?u.18857} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ upperBounds s → b ∈ upperBounds t → a * b ∈ upperBounds (s * t)
mul_mem_upperBounds_mul
hx: ?m.18849
hx
hy: ?m.18855
hy
#align subset_upper_bounds_mul
subset_upperBounds_mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (s t : Set M), upperBounds s * upperBounds t ⊆ upperBounds (s * t)
subset_upperBounds_mul
#align subset_upper_bounds_add
subset_upperBounds_add: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (s t : Set M), upperBounds s + upperBounds t ⊆ upperBounds (s + t)
subset_upperBounds_add
@[
to_additive: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ lowerBounds s → b ∈ lowerBounds t → a + b ∈ lowerBounds (s + t)
to_additive
] theorem
mul_mem_lowerBounds_mul: ∀ {s t : Set M} {a b : M}, a ∈ lowerBounds s → b ∈ lowerBounds t → a * b ∈ lowerBounds (s * t)
mul_mem_lowerBounds_mul
{
s: Set M
s
t: Set M
t
:
Set: Type ?u.19295 → Type ?u.19295
Set
M: Type ?u.19111
M
} {
a: M
a
b: M
b
:
M: Type ?u.19111
M
} (ha :
a: M
a
∈
lowerBounds: {α : Type ?u.19317} → [inst : Preorder α] → Set α → Set α
lowerBounds
s: Set M
s
) (hb :
b: M
b
∈
lowerBounds: {α : Type ?u.19369} → [inst : Preorder α] → Set α → Set α
lowerBounds
t: Set M
t
) :
a: M
a
*
b: M
b
∈
lowerBounds: {α : Type ?u.19456} → [inst : Preorder α] → Set α → Set α
lowerBounds
(
s: Set M
s
*
t: Set M
t
) := @
mul_mem_upperBounds_mul: ∀ {M : Type ?u.19552} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ upperBounds s → b ∈ upperBounds t → a * b ∈ upperBounds (s * t)
mul_mem_upperBounds_mul
M: Type ?u.19111
M
ᵒᵈ _ _ _ _ _ _ _ _ ha hb #align mul_mem_lower_bounds_mul
mul_mem_lowerBounds_mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ lowerBounds s → b ∈ lowerBounds t → a * b ∈ lowerBounds (s * t)
mul_mem_lowerBounds_mul
#align add_mem_lower_bounds_add
add_mem_lowerBounds_add: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M} {a b : M}, a ∈ lowerBounds s → b ∈ lowerBounds t → a + b ∈ lowerBounds (s + t)
add_mem_lowerBounds_add
@[
to_additive: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (s t : Set M), lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)
to_additive
] theorem
subset_lowerBounds_mul: ∀ (s t : Set M), lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
subset_lowerBounds_mul
(
s: Set M
s
t: Set M
t
:
Set: Type ?u.20069 → Type ?u.20069
Set
M: Type ?u.19885
M
) :
lowerBounds: {α : Type ?u.20083} → [inst : Preorder α] → Set α → Set α
lowerBounds
s: Set M
s
*
lowerBounds: {α : Type ?u.20094} → [inst : Preorder α] → Set α → Set α
lowerBounds
t: Set M
t
⊆
lowerBounds: {α : Type ?u.20167} → [inst : Preorder α] → Set α → Set α
lowerBounds
(
s: Set M
s
*
t: Set M
t
) := @
subset_upperBounds_mul: ∀ {M : Type ?u.20236} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (s t : Set M), upperBounds s * upperBounds t ⊆ upperBounds (s * t)
subset_upperBounds_mul
M: Type ?u.19885
M
ᵒᵈ _ _ _ _ _ _ #align subset_lower_bounds_mul
subset_lowerBounds_mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (s t : Set M), lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
subset_lowerBounds_mul
#align subset_lower_bounds_add
subset_lowerBounds_add: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (s t : Set M), lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)
subset_lowerBounds_add
@[
to_additive: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M}, BddAbove s → BddAbove t → BddAbove (s + t)
to_additive
] theorem
BddAbove.mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M}, BddAbove s → BddAbove t → BddAbove (s * t)
BddAbove.mul
{
s: Set M
s
t: Set M
t
:
Set: Type ?u.20736 → Type ?u.20736
Set
M: Type ?u.20552
M
} (
hs: BddAbove s
hs
:
BddAbove: {α : Type ?u.20739} → [inst : Preorder α] → Set α → Prop
BddAbove
s: Set M
s
) (
ht: BddAbove t
ht
:
BddAbove: {α : Type ?u.20765} → [inst : Preorder α] → Set α → Prop
BddAbove
t: Set M
t
) :
BddAbove: {α : Type ?u.20786} → [inst : Preorder α] → Set α → Prop
BddAbove
(
s: Set M
s
*
t: Set M
t
) := (
Nonempty.mul: ∀ {α : Type ?u.20883} [inst : Mul α] {s t : Set α}, Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s * t)
Nonempty.mul
hs: BddAbove s
hs
ht: BddAbove t
ht
).
mono: ∀ {α : Type ?u.20905} {s t : Set α}, s ⊆ t → Set.Nonempty s → Set.Nonempty t
mono
(
subset_upperBounds_mul: ∀ {M : Type ?u.20914} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (s t : Set M), upperBounds s * upperBounds t ⊆ upperBounds (s * t)
subset_upperBounds_mul
s: Set M
s
t: Set M
t
) #align bdd_above.mul
BddAbove.mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M}, BddAbove s → BddAbove t → BddAbove (s * t)
BddAbove.mul
#align bdd_above.add
BddAbove.add: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M}, BddAbove s → BddAbove t → BddAbove (s + t)
BddAbove.add
@[
to_additive: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M}, BddBelow s → BddBelow t → BddBelow (s + t)
to_additive
] theorem
BddBelow.mul: ∀ {s t : Set M}, BddBelow s → BddBelow t → BddBelow (s * t)
BddBelow.mul
{
s: Set M
s
t: Set M
t
:
Set: Type ?u.21233 → Type ?u.21233
Set
M: Type ?u.21049
M
} (
hs: BddBelow s
hs
:
BddBelow: {α : Type ?u.21236} → [inst : Preorder α] → Set α → Prop
BddBelow
s: Set M
s
) (
ht: BddBelow t
ht
:
BddBelow: {α : Type ?u.21262} → [inst : Preorder α] → Set α → Prop
BddBelow
t: Set M
t
) :
BddBelow: {α : Type ?u.21283} → [inst : Preorder α] → Set α → Prop
BddBelow
(
s: Set M
s
*
t: Set M
t
) := (
Nonempty.mul: ∀ {α : Type ?u.21380} [inst : Mul α] {s t : Set α}, Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s * t)
Nonempty.mul
hs: BddBelow s
hs
ht: BddBelow t
ht
).
mono: ∀ {α : Type ?u.21402} {s t : Set α}, s ⊆ t → Set.Nonempty s → Set.Nonempty t
mono
(
subset_lowerBounds_mul: ∀ {M : Type ?u.21411} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (s t : Set M), lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
subset_lowerBounds_mul
s: Set M
s
t: Set M
t
) #align bdd_below.mul
BddBelow.mul: ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Set M}, BddBelow s → BddBelow t → BddBelow (s * t)
BddBelow.mul
#align bdd_below.add
BddBelow.add: ∀ {M : Type u_1} [inst : Add M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass M M (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Set M}, BddBelow s → BddBelow t → BddBelow (s + t)
BddBelow.add
end mul_add section ConditionallyCompleteLattice section Right variable {
ι: Type ?u.22512
ι
G: Type ?u.22515
G
:
Type _: Type (?u.22515+1)
Type _
} [
Group: Type ?u.22518 → Type ?u.22518
Group
G: Type ?u.21549
G
] [
ConditionallyCompleteLattice: Type ?u.21555 → Type ?u.21555
ConditionallyCompleteLattice
G: Type ?u.21549
G
] [
CovariantClass: (M : Type ?u.21559) → (N : Type ?u.21558) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
G: Type ?u.21549
G
G: Type ?u.21549
G
(
Function.swap: {α : Sort ?u.21562} → {β : Sort ?u.21561} → {φ : α → β → Sort ?u.21560} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
Function.swap
(· * ·): G → G → G
(· * ·)
)
(· ≤ ·): G → G → Prop
(· ≤ ·)
] [
Nonempty: Sort ?u.22505 → Prop
Nonempty
ι: Type ?u.21546
ι
] {
f: ι → G
f
:
ι: Type ?u.21546
ι
→
G: Type ?u.21549
G
} @[
to_additive: ∀ {ι : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) + a = ⨆ i, f i + a
to_additive
] theorem
ciSup_mul: ∀ {ι : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) * a = ⨆ i, f i * a
ciSup_mul
(
hf: BddAbove (range f)
hf
:
BddAbove: {α : Type ?u.23478} → [inst : Preorder α] → Set α → Prop
BddAbove
(
Set.range: {α : Type ?u.23498} → {ι : Sort ?u.23497} → (ι → α) → Set α
Set.range
f: ι → G
f
)) (
a: G
a
:
G: Type ?u.22515
G
) : (⨆
i: ?m.23830
i
,
f: ι → G
f
i: ?m.23830
i
) *
a: G
a
= ⨆
i: ?m.23851
i
,
f: ι → G
f
i: ?m.23851
i
*
a: G
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 α
OrderIso.mulRight
a: G
a
).
map_ciSup: ∀ {α : Type ?u.25062} {β : Type ?u.25063} {ι : Sort ?u.25064} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β] [inst_2 : Nonempty ι] (e : α ≃o β) {f : ι → α}, BddAbove (range f) → ↑e (⨆ i, f i) = ⨆ i, ↑e (f i)
map_ciSup
hf: BddAbove (range f)
hf
#align csupr_mul
ciSup_mul: ∀ {ι : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) * a = ⨆ i, f i * a
ciSup_mul
#align csupr_add
ciSup_add: ∀ {ι : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) + a = ⨆ i, f i + a
ciSup_add
@[
to_additive: ∀ {ι : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) - a = ⨆ i, f i - a
to_additive
] theorem
ciSup_div: ∀ {ι : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) / a = ⨆ i, f i / a
ciSup_div
(
hf: BddAbove (range f)
hf
:
BddAbove: {α : Type ?u.26226} → [inst : Preorder α] → Set α → Prop
BddAbove
(
Set.range: {α : Type ?u.26246} → {ι : Sort ?u.26245} → (ι → α) → Set α
Set.range
f: ι → G
f
)) (
a: G
a
:
G: Type ?u.25263
G
) : (⨆
i: ?m.26578
i
,
f: ι → G
f
i: ?m.26578
i
) /
a: G
a
= ⨆
i: ?m.26599
i
,
f: ι → G
f
i: ?m.26599
i
/
a: G
a
:=

Goals accomplished! 🐙
ι: Type u_2

G: Type u_1

inst✝³: Group G

inst✝²: ConditionallyCompleteLattice G

inst✝¹: CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

inst✝: Nonempty ι

f: ι → G

hf: BddAbove (range f)

a: G


(⨆ i, f i) / a = ⨆ i, f i / a

Goals accomplished! 🐙
#align csupr_div
ciSup_div: ∀ {ι : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) / a = ⨆ i, f i / a
ciSup_div
#align csupr_sub
ciSup_sub: ∀ {ι : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (⨆ i, f i) - a = ⨆ i, f i - a
ciSup_sub
end Right section Left variable {
ι: Type ?u.27170
ι
G: Type ?u.27173
G
:
Type _: Type (?u.27173+1)
Type _
} [
Group: Type ?u.27176 → Type ?u.27176
Group
G: Type ?u.27173
G
] [
ConditionallyCompleteLattice: Type ?u.27179 → Type ?u.27179
ConditionallyCompleteLattice
G: Type ?u.27173
G
] [
CovariantClass: (M : Type ?u.28127) → (N : Type ?u.28126) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
G: Type ?u.27173
G
G: Type ?u.28117
G
(· * ·): G → G → G
(· * ·)
(· ≤ ·): G → G → Prop
(· ≤ ·)
] [
Nonempty: Sort ?u.29051 → Prop
Nonempty
ι: Type ?u.28114
ι
] {
f: ι → G
f
:
ι: Type ?u.28114
ι
→
G: Type ?u.27173
G
} @[
to_additive: ∀ {ι : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (a + ⨆ i, f i) = ⨆ i, a + f i
to_additive
] theorem
mul_ciSup: BddAbove (range f) → ∀ (a : G), (a * ⨆ i, f i) = ⨆ i, a * f i
mul_ciSup
(
hf: BddAbove (range f)
hf
:
BddAbove: {α : Type ?u.29058} → [inst : Preorder α] → Set α → Prop
BddAbove
(
Set.range: {α : Type ?u.29078} → {ι : Sort ?u.29077} → (ι → α) → Set α
Set.range
f: ι → G
f
)) (
a: G
a
:
G: Type ?u.28117
G
) : (
a: G
a
* ⨆
i: ?m.29410
i
,
f: ι → G
f
i: ?m.29410
i
) = ⨆
i: ?m.29431
i
,
a: G
a
*
f: ι → G
f
i: ?m.29431
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 α
OrderIso.mulLeft
a: G
a
).
map_ciSup: ∀ {α : Type ?u.30641} {β : Type ?u.30642} {ι : Sort ?u.30643} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β] [inst_2 : Nonempty ι] (e : α ≃o β) {f : ι → α}, BddAbove (range f) → ↑e (⨆ i, f i) = ⨆ i, ↑e (f i)
map_ciSup
hf: BddAbove (range f)
hf
#align mul_csupr
mul_ciSup: ∀ {ι : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (a * ⨆ i, f i) = ⨆ i, a * f i
mul_ciSup
#align add_csupr
add_ciSup: ∀ {ι : Type u_2} {G : Type u_1} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : Nonempty ι] {f : ι → G}, BddAbove (range f) → ∀ (a : G), (a + ⨆ i, f i) = ⨆ i, a + f i
add_ciSup
end Left end ConditionallyCompleteLattice